ex a, A being set st
( ( for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A & [(x 'in' y),F₂(x,y)] in A ) ) & [F₆(),a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F₁((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F₂((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F₃(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) )

F₇() = F₈()

A1: ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A & [(x 'in' y),F₂(x,y)] in A ) ) & [F₆(),F₇()] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F₁((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F₂((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F₃(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) and
A2: ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A & [(x 'in' y),F₂(x,y)] in A ) ) & [F₆(),F₈()] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F₁((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F₂((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F₃(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) )

( ( F₆() is_equality implies F₇(F₆()) = F₁((Var1 F₆()),(Var2 F₆())) ) & ( F₆() is_membership implies F₇(F₆()) = F₂((Var1 F₆()),(Var2 F₆())) ) & ( F₆() is negative implies F₇(F₆()) = F₃(F₇((the_argument_of F₆()))) ) & ( F₆() is conjunctive implies for a, b being set st a = F₇((the_left_argument_of F₆())) & b = F₇((the_right_argument_of F₆())) holds
F₇(F₆()) = F₄(a,b) ) & ( F₆() is universal implies F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) ) )

A1: for H' being ZF-formula
for a being set holds
( a = F₇(H') iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A & [(x 'in' y),F₂(x,y)] in A ) ) & [H',a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F₁((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F₂((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F₃(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) )

P₁[F₆(F₇())]

A1: for H' being ZF-formula
for a being set holds
( a = F₆(H') iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A & [(x 'in' y),F₂(x,y)] in A ) ) & [H',a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F₁((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F₂((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F₃(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) ) and
A2: for x, y being Variable holds
( P₁[F₁(x,y)] & P₁[F₂(x,y)] ) and
A3: for a being set st P₁[a] holds
P₁[F₃(a)] and
A4: for a, b being set st P₁[a] & P₁[b] holds
P₁[F₄(a,b)] and
A5: for a being set
for x being Variable st P₁[a] holds
P₁[F₅(x,a)]

let H be ZF-formula;
func Free H -> set means :Def1: :: ZF_MODEL:def 1
ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,it] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) );
existence
ex b₁, A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b₁] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) ) uniqueness
for b₁, b₂ being set st ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b₁] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) ) & ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b₂] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) ) holds
b₁ = b₂

let H be ZF-formula; :: thesis: ( ( H is_equality implies H₆(H) = H₁( Var1 H, Var2 H) ) & ( H is_membership implies H₆(H) = H₂( Var1 H, Var2 H) ) & ( H is negative implies H₆(H) = H₃(H₆( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₆( the_left_argument_of H) & b = H₆( the_right_argument_of H) holds
H₆(H) = H₄(a,b) ) & ( H is universal implies H₆(H) = H₅( bound_in H,H₆( the_scope_of H)) ) )
thus ( ( H is_equality implies H₆(H) = H₁( Var1 H, Var2 H) ) & ( H is_membership implies H₆(H) = H₂( Var1 H, Var2 H) ) & ( H is negative implies H₆(H) = H₃(H₆( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₆( the_left_argument_of H) & b = H₆( the_right_argument_of H) holds
H₆(H) = H₄(a,b) ) & ( H is universal implies H₆(H) = H₅( bound_in H,H₆( the_scope_of H)) ) ) from ZF_MODEL:sch 3( E , Lm1); :: thesis: verum

let H be ZF-formula;
:: original: Free
redefine func Free H -> Subset of VAR ;
coherence
Free H is Subset of VAR

let D be non empty set ;
func VAL D -> set means :Def2: :: ZF_MODEL:def 2
for a being set holds
( a in it iff a is Function of VAR ,D );
existence
ex b₁ being set st
for a being set holds
( a in b₁ iff a is Function of VAR ,D ) uniqueness
for b₁, b₂ being set st ( for a being set holds
( a in b₁ iff a is Function of VAR ,D ) ) & ( for a being set holds
( a in b₂ iff a is Function of VAR ,D ) ) holds
b₁ = b₂

let D be non empty set ;
cluster VAL D -> non empty ;
coherence
not VAL D is empty

let H be ZF-formula;
let E be non empty set ;
deffunc H₇( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 = f . $2 } ;
deffunc H₈( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 in f . $2 } ;
deffunc H₉( set ) -> set = (VAL E) \ (union {$1});
deffunc H₁₀( set , set ) -> set = (union {$1}) /\ (union {$2});
deffunc H₁₁( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = $2 & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
$1 = y ) holds
g in X ) ) } ;
func St H,E -> set means :Def3: :: ZF_MODEL:def 3
ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ] in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y } ] in A ) ) & [H,it] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H') } ) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H') } ) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) ) } & [(the_scope_of H'),b] in A ) ) ) ) );
existence
ex b₁, A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ] in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y } ] in A ) ) & [H,b₁] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H') } ) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H') } ) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) ) } & [(the_scope_of H'),b] in A ) ) ) ) ) uniqueness
for b₁, b₂ being set st ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ] in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y } ] in A ) ) & [H,b₁] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H') } ) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H') } ) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) ) } & [(the_scope_of H'),b] in A ) ) ) ) ) & ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ] in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y } ] in A ) ) & [H,b₂] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H') } ) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H') } ) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) ) } & [(the_scope_of H'),b] in A ) ) ) ) ) holds
b₁ = b₂

let H be ZF-formula; :: thesis: for E being non empty set holds
( ( H is_equality implies H₁₂(H) = H₇( Var1 H, Var2 H) ) & ( H is_membership implies H₁₂(H) = H₈( Var1 H, Var2 H) ) & ( H is negative implies H₁₂(H) = H₉(H₁₂( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₁₂( the_left_argument_of H) & b = H₁₂( the_right_argument_of H) holds
H₁₂(H) = H₁₀(a,b) ) & ( H is universal implies H₁₂(H) = H₁₁( bound_in H,H₁₂( the_scope_of H)) ) )
let E be non empty set ; :: thesis: ( ( H is_equality implies H₁₂(H) = H₇( Var1 H, Var2 H) ) & ( H is_membership implies H₁₂(H) = H₈( Var1 H, Var2 H) ) & ( H is negative implies H₁₂(H) = H₉(H₁₂( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₁₂( the_left_argument_of H) & b = H₁₂( the_right_argument_of H) holds
H₁₂(H) = H₁₀(a,b) ) & ( H is universal implies H₁₂(H) = H₁₁( bound_in H,H₁₂( the_scope_of H)) ) )
deffunc H₇( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 = f . $2 } ;
deffunc H₈( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 in f . $2 } ;
deffunc H₉( set ) -> set = (VAL E) \ (union {$1});
deffunc H₁₀( set , set ) -> set = (union {$1}) /\ (union {$2});
deffunc H₁₁( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = $2 & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
$1 = y ) holds
g in X ) ) } ;
deffunc H₁₂( ZF-formula) -> set = St $1,E;
A1: for H being ZF-formula
for a being set holds
( a = H₁₂(H) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H₇(x,y)] in A & [(x 'in' y),H₈(x,y)] in A ) ) & [H,a] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = H₇( Var1 H', Var2 H') ) & ( H' is_membership implies a = H₈( Var1 H', Var2 H') ) & ( H' is negative implies ex b being set st
( a = H₉(b) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = H₁₀(b,c) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = H₁₁( bound_in H',b) & [(the_scope_of H'),b] in A ) ) ) ) ) ) by Def3;
thus ( ( H is_equality implies H₁₂(H) = H₇( Var1 H, Var2 H) ) & ( H is_membership implies H₁₂(H) = H₈( Var1 H, Var2 H) ) & ( H is negative implies H₁₂(H) = H₉(H₁₂( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₁₂( the_left_argument_of H) & b = H₁₂( the_right_argument_of H) holds
H₁₂(H) = H₁₀(a,b) ) & ( H is universal implies H₁₂(H) = H₁₁( bound_in H,H₁₂( the_scope_of H)) ) ) from ZF_MODEL:sch 3( E , A1); :: thesis: verum

let H be ZF-formula;
let E be non empty set ;
:: original: St
redefine func St H,E -> Subset of (VAL E);
coherence
St H,E is Subset of (VAL E)

let D be non empty set ;
let f be Function of VAR ,D;
let H be ZF-formula;
pred D,f |= H means :Def4: :: ZF_MODEL:def 4
f in St H,D;

let E be non empty set ;
let H be ZF-formula;
pred E |= H means :Def5: :: ZF_MODEL:def 5
for f being Function of VAR ,E holds E,f |= H;

func the_axiom_of_extensionality -> ZF-formula equals :: ZF_MODEL:def 6
All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1)));
correctness
coherence
All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1))) is ZF-formula;
;
func the_axiom_of_pairs -> ZF-formula equals :: ZF_MODEL:def 7
All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))));
correctness
coherence
All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is ZF-formula;
;
func the_axiom_of_unions -> ZF-formula equals :: ZF_MODEL:def 8
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))));
correctness
coherence
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is ZF-formula;
;
func the_axiom_of_infinity -> ZF-formula equals :: ZF_MODEL:def 9
Ex (x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All (x. 2),(((x. 2) 'in' (x. 0)) => (Ex (x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))));
correctness
coherence
Ex (x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All (x. 2),(((x. 2) 'in' (x. 0)) => (Ex (x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is ZF-formula;
;
func the_axiom_of_power_sets -> ZF-formula equals :: ZF_MODEL:def 10
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))));
correctness
coherence
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is ZF-formula;
;

let H be ZF-formula;
func the_axiom_of_substitution_for H -> ZF-formula equals :: ZF_MODEL:def 11
(All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H))))));
correctness
coherence
(All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)))))) is ZF-formula;
;