Our cookies follow Google AdSense policy.

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.0We 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.1Let 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.2Let 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.3Let 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)).