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 ) -> Element of bool (VAL E) = (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;
defpred S₁[ set ] means $1 is Subset of (VAL 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 being_equality implies a = H₇( Var1 H', Var2 H') ) & ( H' is being_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;

now

let x, y be Variable; :: thesis: ( { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) & { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) )
set X1 = { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ;
{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } c= VAL E

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } or a in VAL E )
assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ; :: thesis: a in VAL E
then ex v1 being Element of VAL E st
( a = v1 & ( for f being Function of VAR ,E st f = v1 holds
f . x = f . y ) ) ;
hence a in VAL E ; :: thesis: verum

end;

hence { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) ; :: thesis: { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x in f . y } is Subset of (VAL E)
set X2 = { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x in f . y } ;
{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x in f . y } c= VAL E

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x in f . y } or a in VAL E )
assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x in f . y } ; :: thesis: a in VAL E
then ex v1 being Element of VAL E st
( a = v1 & ( for f being Function of VAR ,E st f = v1 holds
f . x in f . y ) ) ;
hence a in VAL E ; :: thesis: verum

end;

hence { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) ; :: thesis: verum

end;

then A2: for x, y being Variable holds
( S₁[H₇(x,y)] & S₁[H₈(x,y)] ) ;
A3: for b being set st S₁[b] holds
S₁[H₉(b)] ;
A4: for X, Y being set st S₁[X] & S₁[Y] holds
S₁[H₁₀(X,Y)]

proof

let X, Y be set ; :: thesis: ( S₁[X] & S₁[Y] implies S₁[H₁₀(X,Y)] )
assume ( X is Subset of (VAL E) & Y is Subset of (VAL E) ) ; :: thesis: S₁[H₁₀(X,Y)]
then reconsider X = X as Subset of (VAL E) ;
A5: union {X} = X by ZFMISC_1:31;
(union {X}) /\ (union {Y}) c= VAL E

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (union {X}) /\ (union {Y}) or a in VAL E )
assume a in (union {X}) /\ (union {Y}) ; :: thesis: a in VAL E
then a in X by A5, XBOOLE_0:def 4;
hence a in VAL E ; :: thesis: verum

end;

hence S₁[H₁₀(X,Y)] ; :: thesis: verum

end;

A6: for a being set
for x being Variable st S₁[a] holds
S₁[H₁₁(x,a)]

proof

let a be set ; :: thesis: for x being Variable st S₁[a] holds
S₁[H₁₁(x,a)]
let x be Variable; :: thesis: ( S₁[a] implies S₁[H₁₁(x,a)] )
assume a is Subset of (VAL E) ; :: thesis: S₁[H₁₁(x,a)]
set Y = { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } ;
{ u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } c= VAL E

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } or b in VAL E )
assume b in { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } ; :: thesis: b in VAL E
then ex v1 being Element of VAL E st
( b = v1 & ( for X being set
for f being Function of VAR ,E st X = a & f = v1 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) ) ) ;
hence b in VAL E ; :: thesis: verum

end;

hence S₁[H₁₁(x,a)] ; :: thesis: verum

end;

thus S₁[H₁₂(H)] from ZF_MODEL:sch 4(A1, A2, A3, A4, A6); :: thesis: verum