let x, y be Variable; :: thesis:
let M be non empty set ; :: thesis:
let H be ZF-formula; :: thesis:
let v be Function of VAR ,M; :: thesis:
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:
A2: ( ( x1 = y or x1 <> y ) & ( x2 = y or x2 <> y ) ) ;
thus S₁[x1 '=' x2] :: thesis:

proof

assume not x in variables_in (x1 '=' x2) ; :: thesis:
let v be Function of VAR ,M; :: thesis:
consider y1, y2 being Variable such that
A3: ( ( 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 A2;
A4: (x1 '=' x2) / y,x = y1 '=' y2 by A3, ZF_LANG1:166;
A5: ( (v / y,(v . x)) . x1 = v . y1 & (v / y,(v . x)) . x2 = v . y2 ) by A3, FUNCT_7:34, FUNCT_7:130;
thus ( M,v |= (x1 '=' x2) / y,x implies M,v / y,(v . x) |= x1 '=' x2 ) :: thesis:

proof

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

end;

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

end;

assume not x in variables_in (x1 'in' x2) ; :: thesis:
let v be Function of VAR ,M; :: thesis:
consider y1, y2 being Variable such that
A6: ( ( 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 A2;
A7: (x1 'in' x2) / y,x = y1 'in' y2 by A6, ZF_LANG1:168;
A8: ( (v / y,(v . x)) . x1 = v . y1 & (v / y,(v . x)) . x2 = v . y2 ) by A6, FUNCT_7:34, FUNCT_7:130;
thus ( M,v |= (x1 'in' x2) / y,x implies M,v / y,(v . x) |= x1 'in' x2 ) :: thesis:

proof

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

end;

assume M,v / y,(v . x) |= x1 'in' x2 ; :: thesis:
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 A7, A8, ZF_MODEL:13; :: thesis:

end;

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

proof

let H be ZF-formula; :: thesis:
assume A10: ( 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:
assume A11: not x in variables_in ('not' H) ; :: thesis:
let v be Function of VAR ,M; :: thesis:
thus ( M,v |= ('not' H) / y,x implies M,v / y,(v . x) |= 'not' H ) :: thesis:

proof

assume M,v |= ('not' H) / y,x ; :: thesis:
then M,v |= 'not' (H / y,x) by ZF_LANG1:170;
then not M,v |= H / y,x by ZF_MODEL:14;
then not M,v / y,(v . x) |= H by A10, A11, ZF_LANG1:153;
hence M,v / y,(v . x) |= 'not' H by ZF_MODEL:14; :: thesis:

end;

assume M,v / y,(v . x) |= 'not' H ; :: thesis:
then not M,v / y,(v . x) |= H by ZF_MODEL:14;
then not M,v |= H / y,x by A10, A11, ZF_LANG1:153;
then M,v |= 'not' (H / y,x) by ZF_MODEL:14;
hence M,v |= ('not' H) / y,x by ZF_LANG1:170; :: thesis:

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:
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:
assume not x in variables_in (H1 '&' H2) ; :: thesis:
then A15: not x in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:154;
let v be Function of VAR ,M; :: thesis:
thus ( M,v |= (H1 '&' H2) / y,x implies M,v / y,(v . x) |= H1 '&' H2 ) :: thesis:

proof

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

end;

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

end;

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

proof

let H be ZF-formula; :: thesis:
let z be Variable; :: thesis:
assume A17: ( 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:
assume A18: not x in variables_in (All z,H) ; :: thesis:
Free (All z,H) c= variables_in (All z,H) by ZF_LANG1:164;
then A19: not x in Free (All z,H) by A18;
A20: not x in (variables_in H) \/ {z} by A18, ZF_LANG1:155;
then ( not x in variables_in H & not x in {z} & Free H c= variables_in H ) by XBOOLE_0:def 3, ZF_LANG1:164;
then A21: ( x <> z & not x in Free H & ( for v being Function of VAR ,M holds
( M,v |= H / y,x iff M,v / y,(v . x) |= H ) ) ) by A17, TARSKI:def 1;
( z = y or z <> y ) ;
then consider s being Variable such that
A22: ( ( z = y & s = x ) or ( z <> y & s = z ) ) ;
let v be Function of VAR ,M; :: thesis:
thus ( M,v |= (All z,H) / y,x implies M,v / y,(v . x) |= All z,H ) :: thesis:

proof

assume M,v |= (All z,H) / y,x ; :: thesis:
then A23: M,v |= All s,(H / y,x) by A22, ZF_LANG1:173, ZF_LANG1:174;

A24: now

assume A25: ( z = y & s = x ) ; :: thesis:

now

let m be Element of M; :: thesis:
M,v / x,m |= H / y,x by A23, A25, ZF_LANG1:80;
then ( M,(v / x,m) / y,((v / x,m) . x) |= H & (v / x,m) . x = m & (v / x,m) / y,m = (v / y,m) / x,m ) by A21, A25, FUNCT_7:35, FUNCT_7:130;
then M,(v / y,m) / x,m |= All x,H by A21, ZFMODEL1:10;
then ( ((v / y,m) / x,m) / x,((v / y,m) . x) = (v / y,m) / x,((v / y,m) . x) & M,((v / y,m) / x,m) / x,((v / y,m) . x) |= H ) by FUNCT_7:36, ZF_LANG1:80;
hence M,v / y,m |= H by FUNCT_7:37; :: thesis:

end;

then M,v |= All y,H by ZF_LANG1:80;
hence M,v / y,(v . x) |= All z,H by A25, ZF_LANG1:81; :: thesis:

end;

now

assume A26: ( z <> y & s = z ) ; :: thesis:

now

let m be Element of M; :: thesis:
M,v / z,m |= H / y,x by A23, A26, ZF_LANG1:80;
then ( M,(v / z,m) / y,((v / z,m) . x) |= H & (v / z,m) . x = v . x & (v / z,m) / y,(v . x) = (v / y,(v . x)) / z,m ) by A21, A26, FUNCT_7:35, FUNCT_7:34;
hence M,(v / y,(v . x)) / z,m |= H ; :: thesis:

end;

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

end;

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

end;

assume A27: M,v / y,(v . x) |= All z,H ; :: thesis:

A28: now

assume A29: ( z = y & s = x ) ; :: thesis:
then M,v |= All y,H by A27, ZF_LANG1:81;
then A30: M,v |= All x,(All y,H) by A19, A29, ZFMODEL1:10;

now

let m be Element of M; :: thesis:
M,v / x,m |= All y,H by A30, ZF_LANG1:80;
then ( M,(v / x,m) / y,m |= H & (v / x,m) . x = m ) by ZF_LANG1:80, FUNCT_7:130;
hence M,v / x,m |= H / y,x by A17, A20, XBOOLE_0:def 3; :: thesis:

end;

then M,v |= All x,(H / y,x) by ZF_LANG1:80;
hence M,v |= (All z,H) / y,x by A29, ZF_LANG1:174; :: thesis:

end;

now

assume A31: ( z <> y & s = z ) ; :: thesis:

now

let m be Element of M; :: thesis:
M,(v / y,(v . x)) / z,m |= H by A27, ZF_LANG1:80;
then M,(v / z,m) / y,(v . x) |= H by A31, FUNCT_7:35;
then M,(v / z,m) / y,((v / z,m) . x) |= H by A21, FUNCT_7:34;
hence M,v / z,m |= H / y,x by A17, A20, XBOOLE_0:def 3; :: thesis:

end;

then M,v |= All z,(H / y,x) by ZF_LANG1:80;
hence M,v |= (All z,H) / y,x by A31, ZF_LANG1:173; :: thesis:

end;

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

end;

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