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 S1[ 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
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1, x2 be Variable; :: thesis: ( S1[x1 '=' x2] & S1[x1 'in' x2] )
A2: ( x2 = y or x2 <> y ) ;
A3: ( x1 = y or x1 <> y ) ;
thus S1[x1 '=' x2] :: thesis: S1[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 ;
A6: (v / (y,(v . x))) . x1 = v . y1 by ;
A7: (x1 '=' x2) / (y,x) = y1 '=' y2 by ;
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 ;
hence M,v / (y,(v . x)) |= x1 '=' x2 by ; :: 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 ; :: 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 ;
A10: (v / (y,(v . x))) . x2 = v . y2 by ;
A11: (x1 'in' x2) / (y,x) = y1 'in' y2 by ;
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 ;
hence M,v / (y,(v . x)) |= x1 'in' x2 by ; :: 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 ; :: thesis: verum
end;
A12: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; :: thesis: ( S1[H1] & S1[H2] implies S1[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: S1[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 () \/ () 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 ;
M,v |= H1 / (y,x) by ;
then M,v / (y,(v . x)) |= H1 by ;
hence M,v / (y,(v . x)) |= H1 '&' H2 by ; :: 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 ;
M,v / (y,(v . x)) |= H1 by ;
then M,v |= H1 / (y,x) by ;
then M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by ;
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 S1[H] holds
S1[ All (z,H)]
proof
let H be ZF-formula; :: thesis: for z being Variable st S1[H] holds
S1[ All (z,H)]

let z be Variable; :: thesis: ( S1[H] implies S1[ 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: S1[ 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 () \/ {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 ;
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 ;
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 ;
then A32: M,(v / (x,m)) / (y,((v / (x,m)) . x)) |= H by ;
(v / (x,m)) / (y,m) = (v / (y,m)) / (x,m) by ;
then M,(v / (y,m)) / (x,m) |= All (x,H) by ;
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 ; :: thesis: verum
end;
then M,v |= All (y,H) by ZF_LANG1:71;
hence M,v / (y,(v . x)) |= All (z,H) by ; :: 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 ;
then A36: M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by ;
(v / (z,m)) . x = v . x by ;
hence M,(v / (y,(v . x))) / (z,m) |= H by ; :: 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 ; :: 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 ;
then A41: M,v |= All (x,(All (y,H))) by ;
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 ;
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 ; :: thesis: verum
end;
then M,v |= All (x,(H / (y,x))) by ZF_LANG1:71;
hence M,v |= (All (z,H)) / (y,x) by ; :: 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 ;
then M,(v / (z,m)) / (y,(v . x)) |= H by ;
then M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by ;
hence M,v / (z,m) |= H / (y,x) by ; :: thesis: verum
end;
then M,v |= All (z,(H / (y,x))) by ZF_LANG1:71;
hence M,v |= (All (z,H)) / (y,x) by ; :: thesis: verum
end;
hence M,v |= (All (z,H)) / (y,x) by ; :: thesis: verum
end;
A44: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; :: thesis: ( S1[H] implies S1[ '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: S1[ 'not' H]
assume A46: not x in variables_in () ; :: thesis: for v being Function of VAR,M holds
( M,v |= () / (y,x) iff M,v / (y,(v . x)) |= 'not' H )

let v be Function of VAR,M; :: thesis: ( M,v |= () / (y,x) iff M,v / (y,(v . x)) |= 'not' H )
thus ( M,v |= () / (y,x) implies M,v / (y,(v . x)) |= 'not' H ) :: thesis: ( M,v / (y,(v . x)) |= 'not' H implies M,v |= () / (y,x) )
proof
assume M,v |= () / (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 ;
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 |= () / (y,x)
then not M,v / (y,(v . x)) |= H by ZF_MODEL:14;
then not M,v |= H / (y,x) by ;
then M,v |= 'not' (H / (y,x)) by ZF_MODEL:14;
hence M,v |= () / (y,x) by ZF_LANG1:156; :: thesis: verum
end;
for H being ZF-formula holds S1[H] from hence ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: verum