let H be ZF-formula; :: thesis:
let M be non empty set ; :: thesis:
defpred S₁[ ZF-formula] means for v, v9 being Function of VAR,M st ( for x being Variable st x in Free $1 holds
v9 . x = v . x ) & M,v |= $1 holds
M,v9 |= $1;
A1: for H1, H2 being ZF-formula st S₁[H1] & S₁[H2] holds
S₁[H1 '&' H2]

let H1, H2 be ZF-formula; :: thesis:
assume that
A2: S₁[H1] and
A3: S₁[H2] ; :: thesis:
let v, v9 be Function of VAR,M; :: thesis:
assume A4: for x being Variable st x in Free (H1 '&' H2) holds
v9 . x = v . x ; :: thesis:
A5: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by Th61;

A6: now :: thesis:

let x be Variable; :: thesis:
assume x in Free H2 ; :: thesis:
then x in Free (H1 '&' H2) by A5, XBOOLE_0:def 3;
hence v9 . x = v . x by A4; :: thesis:

end;

assume A7: M,v |= H1 '&' H2 ; :: thesis:
then M,v |= H2 by ZF_MODEL:15;
then A8: M,v9 |= H2 by A3, A6;

A9: now :: thesis:

let x be Variable; :: thesis:
assume x in Free H1 ; :: thesis:
then x in Free (H1 '&' H2) by A5, XBOOLE_0:def 3;
hence v9 . x = v . x by A4; :: thesis:

end;

M,v |= H1 by A7, ZF_MODEL:15;
then M,v9 |= H1 by A2, A9;
hence M,v9 |= H1 '&' H2 by A8, ZF_MODEL:15; :: thesis:

end;

A10: for x1, x2 being Variable holds
( S₁[x1 '=' x2] & S₁[x1 'in' x2] )

let x1, x2 be Variable; :: thesis:
A11: Free (x1 '=' x2) = {x1,x2} by Th58;
thus S₁[x1 '=' x2] :: thesis:

let v, v9 be Function of VAR,M; :: thesis:
assume A12: for x being Variable st x in Free (x1 '=' x2) holds
v9 . x = v . x ; :: thesis:
x2 in Free (x1 '=' x2) by A11, TARSKI:def 2;
then A13: v9 . x2 = v . x2 by A12;
assume M,v |= x1 '=' x2 ; :: thesis:
then A14: v . x1 = v . x2 by ZF_MODEL:12;
x1 in Free (x1 '=' x2) by A11, TARSKI:def 2;
then v9 . x1 = v . x1 by A12;
hence M,v9 |= x1 '=' x2 by A14, A13, ZF_MODEL:12; :: thesis:

end;

let v, v9 be Function of VAR,M; :: thesis:
assume A15: for x being Variable st x in Free (x1 'in' x2) holds
v9 . x = v . x ; :: thesis:
A16: Free (x1 'in' x2) = {x1,x2} by Th59;
then x2 in Free (x1 'in' x2) by TARSKI:def 2;
then A17: v9 . x2 = v . x2 by A15;
assume M,v |= x1 'in' x2 ; :: thesis:
then A18: v . x1 in v . x2 by ZF_MODEL:13;
x1 in Free (x1 'in' x2) by A16, TARSKI:def 2;
then v9 . x1 = v . x1 by A15;
hence M,v9 |= x1 'in' x2 by A18, A17, ZF_MODEL:13; :: thesis:

end;

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

let H be ZF-formula; :: thesis:
let x1 be Variable; :: thesis:
assume A20: S₁[H] ; :: thesis:
let v, v9 be Function of VAR,M; :: thesis:
assume that
A21: for x being Variable st x in Free (All (x1,H)) holds
v9 . x = v . x and
A22: M,v |= All (x1,H) ; :: thesis:

let m be Element of M; :: thesis:
A23: Free (All (x1,H)) = (Free H) \ {x1} by Th62;

A24: now :: thesis:

let x be Variable; :: thesis:
assume x in Free H ; :: thesis:
then ( ( x in Free (All (x1,H)) & not x in {x1} ) or x in {x1} ) by A23, XBOOLE_0:def 5;
then ( ( v9 . x = v . x & x <> x1 ) or x = x1 ) by A21, TARSKI:def 1;
then ( ( (v9 / (x1,m)) . x = v . x & v . x = (v / (x1,m)) . x ) or ( (v / (x1,m)) . x = m & (v9 / (x1,m)) . x = m ) ) by FUNCT_7:32, FUNCT_7:128;
hence (v9 / (x1,m)) . x = (v / (x1,m)) . x ; :: thesis:

end;

M,v / (x1,m) |= H by A22, Th71;
hence M,v9 / (x1,m) |= H by A20, A24; :: thesis:

end;

hence M,v9 |= All (x1,H) by Th71; :: thesis:

end;

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

let H be ZF-formula; :: thesis:
assume A26: S₁[H] ; :: thesis:
let v, v9 be Function of VAR,M; :: thesis:
assume A27: for x being Variable st x in Free ('not' H) holds
v9 . x = v . x ; :: thesis:

A28: now :: thesis:

let x be Variable; :: thesis:
assume x in Free H ; :: thesis:
then x in Free ('not' H) by Th60;
hence v . x = v9 . x by A27; :: thesis:

end;

assume M,v |= 'not' H ; :: thesis:
then not M,v |= H by ZF_MODEL:14;
then not M,v9 |= H by A26, A28;
hence M,v9 |= 'not' H by ZF_MODEL:14; :: thesis:

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A10, A25, A1, A19);
hence for v, v9 being Function of VAR,M st ( for x being Variable st x in Free H holds
v9 . x = v . x ) & M,v |= H holds
M,v9 |= H ; :: thesis: