let x, y be Variable; :: thesis: for M being non empty set
for H being ZF-formula
for v being Function of VAR,M st not x in variables_in H holds
( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )
let M be non empty set ; :: thesis: for H being ZF-formula
for v being Function of VAR,M st not x in variables_in H holds
( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )
let H be ZF-formula; :: thesis: for v being Function of VAR,M st not x in variables_in H holds
( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )
let v be Function of VAR,M; :: thesis: ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) )
defpred S₁[ ZF-formula] means ( not x in variables_in $1 implies for v being Function of VAR,M holds
( M,v |= $1 / (y,x) iff M,v / (y,(v . x)) |= $1 ) );
A1: for x1, x2 being Variable holds
( S₁[x1 '=' x2] & S₁[x1 'in' x2] )

proof

let x1, x2 be Variable; :: thesis: ( S₁[x1 '=' x2] & S₁[x1 'in' x2] )
A2: ( x2 = y or x2 <> y ) ;
A3: ( x1 = y or x1 <> y ) ;
thus S₁[x1 '=' x2] :: thesis: S₁[x1 'in' x2]

proof

assume not x in variables_in (x1 '=' x2) ; :: thesis: for v being Function of VAR,M holds
( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )
let v be Function of VAR,M; :: thesis: ( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )
consider y1, y2 being Variable such that
A4: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;
A5: (v / (y,(v . x))) . x2 = v . y2 by A4, FUNCT_7:32, FUNCT_7:128;
A6: (v / (y,(v . x))) . x1 = v . y1 by A4, FUNCT_7:32, FUNCT_7:128;
A7: (x1 '=' x2) / (y,x) = y1 '=' y2 by A4, ZF_LANG1:152;
thus ( M,v |= (x1 '=' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 '=' x2 ) :: thesis: ( M,v / (y,(v . x)) |= x1 '=' x2 implies M,v |= (x1 '=' x2) / (y,x) )

proof

assume M,v |= (x1 '=' x2) / (y,x) ; :: thesis: M,v / (y,(v . x)) |= x1 '=' x2
then v . y1 = v . y2 by A7, ZF_MODEL:12;
hence M,v / (y,(v . x)) |= x1 '=' x2 by A6, A5, ZF_MODEL:12; :: thesis: verum

end;

assume M,v / (y,(v . x)) |= x1 '=' x2 ; :: thesis: M,v |= (x1 '=' x2) / (y,x)
then (v / (y,(v . x))) . x1 = (v / (y,(v . x))) . x2 by ZF_MODEL:12;
hence M,v |= (x1 '=' x2) / (y,x) by A7, A6, A5, ZF_MODEL:12; :: thesis: verum

end;

consider y1, y2 being Variable such that
A8: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;
assume not x in variables_in (x1 'in' x2) ; :: thesis: for v being Function of VAR,M holds
( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )
let v be Function of VAR,M; :: thesis: ( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )
A9: (v / (y,(v . x))) . x1 = v . y1 by A8, FUNCT_7:32, FUNCT_7:128;
A10: (v / (y,(v . x))) . x2 = v . y2 by A8, FUNCT_7:32, FUNCT_7:128;
A11: (x1 'in' x2) / (y,x) = y1 'in' y2 by A8, ZF_LANG1:154;
thus ( M,v |= (x1 'in' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 'in' x2 ) :: thesis: ( M,v / (y,(v . x)) |= x1 'in' x2 implies M,v |= (x1 'in' x2) / (y,x) )

proof

assume M,v |= (x1 'in' x2) / (y,x) ; :: thesis: M,v / (y,(v . x)) |= x1 'in' x2
then v . y1 in v . y2 by A11, ZF_MODEL:13;
hence M,v / (y,(v . x)) |= x1 'in' x2 by A9, A10, ZF_MODEL:13; :: thesis: verum

end;

assume M,v / (y,(v . x)) |= x1 'in' x2 ; :: thesis: M,v |= (x1 'in' x2) / (y,x)
then (v / (y,(v . x))) . x1 in (v / (y,(v . x))) . x2 by ZF_MODEL:13;
hence M,v |= (x1 'in' x2) / (y,x) by A11, A9, A10, ZF_MODEL:13; :: thesis: verum

end;

A12: for H1, H2 being ZF-formula st S₁[H1] & S₁[H2] holds
S₁[H1 '&' H2]

proof

let H1, H2 be ZF-formula; :: thesis: ( S₁[H1] & S₁[H2] implies S₁[H1 '&' H2] )
assume that
A13: ( not x in variables_in H1 implies for v being Function of VAR,M holds
( M,v |= H1 / (y,x) iff M,v / (y,(v . x)) |= H1 ) ) and
A14: ( not x in variables_in H2 implies for v being Function of VAR,M holds
( M,v |= H2 / (y,x) iff M,v / (y,(v . x)) |= H2 ) ) ; :: thesis: S₁[H1 '&' H2]
assume not x in variables_in (H1 '&' H2) ; :: thesis: for v being Function of VAR,M holds
( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )
then A15: not x in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;
let v be Function of VAR,M; :: thesis: ( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )
thus ( M,v |= (H1 '&' H2) / (y,x) implies M,v / (y,(v . x)) |= H1 '&' H2 ) :: thesis: ( M,v / (y,(v . x)) |= H1 '&' H2 implies M,v |= (H1 '&' H2) / (y,x) )

proof

assume M,v |= (H1 '&' H2) / (y,x) ; :: thesis: M,v / (y,(v . x)) |= H1 '&' H2
then A16: M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by ZF_LANG1:158;
then M,v |= H2 / (y,x) by ZF_MODEL:15;
then A17: M,v / (y,(v . x)) |= H2 by A14, A15, XBOOLE_0:def 3;
M,v |= H1 / (y,x) by A16, ZF_MODEL:15;
then M,v / (y,(v . x)) |= H1 by A13, A15, XBOOLE_0:def 3;
hence M,v / (y,(v . x)) |= H1 '&' H2 by A17, ZF_MODEL:15; :: thesis: verum

end;

assume A18: M,v / (y,(v . x)) |= H1 '&' H2 ; :: thesis: M,v |= (H1 '&' H2) / (y,x)
then M,v / (y,(v . x)) |= H2 by ZF_MODEL:15;
then A19: M,v |= H2 / (y,x) by A14, A15, XBOOLE_0:def 3;
M,v / (y,(v . x)) |= H1 by A18, ZF_MODEL:15;
then M,v |= H1 / (y,x) by A13, A15, XBOOLE_0:def 3;
then M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by A19, ZF_MODEL:15;
hence M,v |= (H1 '&' H2) / (y,x) by ZF_LANG1:158; :: thesis: verum

end;

A20: for H being ZF-formula
for z being Variable st S₁[H] holds
S₁[ All (z,H)]

proof

let H be ZF-formula; :: thesis: for z being Variable st S₁[H] holds
S₁[ All (z,H)]
let z be Variable; :: thesis: ( S₁[H] implies S₁[ All (z,H)] )
assume A21: ( not x in variables_in H implies for v being Function of VAR,M holds
( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: S₁[ All (z,H)]
( z = y or z <> y ) ;
then consider s being Variable such that
A22: ( ( z = y & s = x ) or ( z <> y & s = z ) ) ;
assume A23: not x in variables_in (All (z,H)) ; :: thesis: for v being Function of VAR,M holds
( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )
then A24: not x in (variables_in H) \/ {z} by ZF_LANG1:142;
then not x in {z} by XBOOLE_0:def 3;
then A25: x <> z by TARSKI:def 1;
let v be Function of VAR,M; :: thesis: ( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )
Free H c= variables_in H by ZF_LANG1:151;
then A26: not x in Free H by A24, XBOOLE_0:def 3;
thus ( M,v |= (All (z,H)) / (y,x) implies M,v / (y,(v . x)) |= All (z,H) ) :: thesis: ( M,v / (y,(v . x)) |= All (z,H) implies M,v |= (All (z,H)) / (y,x) )

proof

assume M,v |= (All (z,H)) / (y,x) ; :: thesis: M,v / (y,(v . x)) |= All (z,H)
then A27: M,v |= All (s,(H / (y,x))) by A22, ZF_LANG1:159, ZF_LANG1:160;

A28: now :: thesis: ( z = y & s = x implies M,v / (y,(v . x)) |= All (z,H) )

assume that
A29: z = y and
A30: s = x ; :: thesis: M,v / (y,(v . x)) |= All (z,H)

now :: thesis: for m being Element of M holds M,v / (y,m) |= H

let m be Element of M; :: thesis: M,v / (y,m) |= H
A31: (v / (x,m)) . x = m by FUNCT_7:128;
M,v / (x,m) |= H / (y,x) by A27, A30, ZF_LANG1:71;
then A32: M,(v / (x,m)) / (y,((v / (x,m)) . x)) |= H by A21, A24, XBOOLE_0:def 3;
(v / (x,m)) / (y,m) = (v / (y,m)) / (x,m) by A25, A29, FUNCT_7:33;
then M,(v / (y,m)) / (x,m) |= All (x,H) by A26, A32, A31, ZFMODEL1:10;
then A33: M,((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) |= H by ZF_LANG1:71;
((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) = (v / (y,m)) / (x,((v / (y,m)) . x)) by FUNCT_7:34;
hence M,v / (y,m) |= H by A33, FUNCT_7:35; :: thesis: verum

end;

then M,v |= All (y,H) by ZF_LANG1:71;
hence M,v / (y,(v . x)) |= All (z,H) by A29, ZF_LANG1:72; :: thesis: verum

end;

now :: thesis: ( z <> y & s = z implies M,v / (y,(v . x)) |= All (z,H) )

assume that
A34: z <> y and
A35: s = z ; :: thesis: M,v / (y,(v . x)) |= All (z,H)

now :: thesis: for m being Element of M holds M,(v / (y,(v . x))) / (z,m) |= H

let m be Element of M; :: thesis: M,(v / (y,(v . x))) / (z,m) |= H
M,v / (z,m) |= H / (y,x) by A27, A35, ZF_LANG1:71;
then A36: M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A21, A24, XBOOLE_0:def 3;
(v / (z,m)) . x = v . x by A25, FUNCT_7:32;
hence M,(v / (y,(v . x))) / (z,m) |= H by A34, A36, FUNCT_7:33; :: thesis: verum

end;

hence M,v / (y,(v . x)) |= All (z,H) by ZF_LANG1:71; :: thesis: verum

end;

hence M,v / (y,(v . x)) |= All (z,H) by A22, A28; :: thesis: verum

end;

assume A37: M,v / (y,(v . x)) |= All (z,H) ; :: thesis: M,v |= (All (z,H)) / (y,x)
Free (All (z,H)) c= variables_in (All (z,H)) by ZF_LANG1:151;
then A38: not x in Free (All (z,H)) by A23;

A39: now :: thesis: ( z = y & s = x implies M,v |= (All (z,H)) / (y,x) )

assume that
A40: z = y and
s = x ; :: thesis: M,v |= (All (z,H)) / (y,x)
M,v |= All (y,H) by A37, A40, ZF_LANG1:72;
then A41: M,v |= All (x,(All (y,H))) by A38, A40, ZFMODEL1:10;

now :: thesis: for m being Element of M holds M,v / (x,m) |= H / (y,x)

let m be Element of M; :: thesis: M,v / (x,m) |= H / (y,x)
M,v / (x,m) |= All (y,H) by A41, ZF_LANG1:71;
then A42: M,(v / (x,m)) / (y,m) |= H by ZF_LANG1:71;
(v / (x,m)) . x = m by FUNCT_7:128;
hence M,v / (x,m) |= H / (y,x) by A21, A24, A42, XBOOLE_0:def 3; :: thesis: verum

end;

then M,v |= All (x,(H / (y,x))) by ZF_LANG1:71;
hence M,v |= (All (z,H)) / (y,x) by A40, ZF_LANG1:160; :: thesis: verum

end;

now :: thesis: ( z <> y & s = z implies M,v |= (All (z,H)) / (y,x) )

assume that
A43: z <> y and
s = z ; :: thesis: M,v |= (All (z,H)) / (y,x)

now :: thesis: for m being Element of M holds M,v / (z,m) |= H / (y,x)

let m be Element of M; :: thesis: M,v / (z,m) |= H / (y,x)
M,(v / (y,(v . x))) / (z,m) |= H by A37, ZF_LANG1:71;
then M,(v / (z,m)) / (y,(v . x)) |= H by A43, FUNCT_7:33;
then M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A25, FUNCT_7:32;
hence M,v / (z,m) |= H / (y,x) by A21, A24, XBOOLE_0:def 3; :: thesis: verum

end;

then M,v |= All (z,(H / (y,x))) by ZF_LANG1:71;
hence M,v |= (All (z,H)) / (y,x) by A43, ZF_LANG1:159; :: thesis: verum

end;

hence M,v |= (All (z,H)) / (y,x) by A22, A39; :: thesis: verum

end;

A44: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H]

proof

let H be ZF-formula; :: thesis: ( S₁[H] implies S₁[ 'not' H] )
assume A45: ( not x in variables_in H implies for v being Function of VAR,M holds
( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: S₁[ 'not' H]
assume A46: not x in variables_in ('not' H) ; :: thesis: for v being Function of VAR,M holds
( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )
let v be Function of VAR,M; :: thesis: ( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )
thus ( M,v |= ('not' H) / (y,x) implies M,v / (y,(v . x)) |= 'not' H ) :: thesis: ( M,v / (y,(v . x)) |= 'not' H implies M,v |= ('not' H) / (y,x) )

proof

assume M,v |= ('not' H) / (y,x) ; :: thesis: M,v / (y,(v . x)) |= 'not' H
then M,v |= 'not' (H / (y,x)) by ZF_LANG1:156;
then not M,v |= H / (y,x) by ZF_MODEL:14;
then not M,v / (y,(v . x)) |= H by A45, A46, ZF_LANG1:140;
hence M,v / (y,(v . x)) |= 'not' H by ZF_MODEL:14; :: thesis: verum

end;

assume M,v / (y,(v . x)) |= 'not' H ; :: thesis: M,v |= ('not' H) / (y,x)
then not M,v / (y,(v . x)) |= H by ZF_MODEL:14;
then not M,v |= H / (y,x) by A45, A46, ZF_LANG1:140;
then M,v |= 'not' (H / (y,x)) by ZF_MODEL:14;
hence M,v |= ('not' H) / (y,x) by ZF_LANG1:156; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A1, A44, A12, A20);
hence ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: verum