iBet uBet web content aggregator. Adding the entire web to your favor.
Link to original content: http://www.apronus.com/provenmath/axioms.htm
Axiom ZF1 - Extensionality.
If x and y are sets then x = y <=> ( /\(z) z:-x <=> z:-y ).
Axiom ZF2 - Empty set.
There exists a set y such that /\(x) !(x:-y).
Definition S.A.0
We define that O = y if and only if /\(x) !(x:-y).
This definition is correct because y is unique by Axiom ZF1.
Axiom ZF3 - Unordered pairs.
If x,y are sets then there exists a set z such that
/\(a) (a:-z <=> (a = x or a = y)).
Definition S.A.1
Let x,y be sets.
We define that
{x,y} = z if and only if /\(a) (a:-z <=> (a = x or a = y)).
We define that {x} = {x,x}.
This definition is correct because z is unique by Axiom ZF1.
Axiom ZF4 - Selection.
If z,y1,y2, ..., yn are sets and P is a well-formed formula
containing variables 'y1', 'y2', ..., 'yn' and a free variable 'x'
and doesn't contain other free variables then
there exits a set y such that
/\(x) ( x:-y <=> (x:-z and P) ).
Definition S.A.2
Let z,y1, ...,yn be sets and let P be a well-formed formula as above.
We define that
{x:-z | P} = y if and only if /\(x) ( x:-y <=> (x:-z and P) ).
This definition is correct because y is unique by Axiom ZF1.
Remark: Compare with Definition S.C.15.
Axiom ZF5 - Union.
If x is a set then there exists a set y such that /\(a)
( a:-y <=> (\/(z) z:-x and a:-z) ).
Definition S.A.3
Let x be a set.
We define that
u(x) = y if and only if /\(a) ( a:-y <=> (\/(z) z:-x and a:-z) ).
This definition is correct because y is unique by Axiom ZF1.
Axiom ZF6 - Power set.
If x is a set then there exists a set z such that
/\(y)( y:-z <=> ( /\(a) (a:-y => a:-x) ) ).
Axiom ZF7 - Infinity.
There exists a set m such that O:-m and /\(x) (x:-m => u({x,{x}}):-m).
Axiom ZF9 - Regularity.
If x is a set and x != O then \/(y) (y:-x and /\(a) !(a:-x and a:-y)).