let H be ZF-formula; :: thesis: for M being non empty set
for v, v' being Function of VAR ,M st ( for x being Variable st x in Free H holds
v' . x = v . x ) & M,v |= H holds
M,v' |= H
let M be non empty set ; :: thesis: for v, v' being Function of VAR ,M st ( for x being Variable st x in Free H holds
v' . x = v . x ) & M,v |= H holds
M,v' |= H
defpred S₁[ ZF-formula] means for v, v' being Function of VAR ,M st ( for x being Variable st x in Free $1 holds
v' . x = v . x ) & M,v |= $1 holds
M,v' |= $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: ( Free (x1 '=' x2) = {x1,x2} & Free (x1 'in' x2) = {x1,x2} ) by Th63, Th64;
thus S₁[x1 '=' x2] :: thesis: S₁[x1 'in' x2]

proof

let v, v' be Function of VAR ,M; :: thesis: ( ( for x being Variable st x in Free (x1 '=' x2) holds
v' . x = v . x ) & M,v |= x1 '=' x2 implies M,v' |= x1 '=' x2 )
assume A3: for x being Variable st x in Free (x1 '=' x2) holds
v' . x = v . x ; :: thesis: ( not M,v |= x1 '=' x2 or M,v' |= x1 '=' x2 )
assume M,v |= x1 '=' x2 ; :: thesis: M,v' |= x1 '=' x2
then A4: v . x1 = v . x2 by ZF_MODEL:12;
( x1 in Free (x1 '=' x2) & x2 in Free (x1 '=' x2) ) by A2, TARSKI:def 2;
then ( v' . x1 = v . x1 & v' . x2 = v . x2 ) by A3;
hence M,v' |= x1 '=' x2 by A4, ZF_MODEL:12; :: thesis: verum

end;

let v, v' be Function of VAR ,M; :: thesis: ( ( for x being Variable st x in Free (x1 'in' x2) holds
v' . x = v . x ) & M,v |= x1 'in' x2 implies M,v' |= x1 'in' x2 )
assume A5: for x being Variable st x in Free (x1 'in' x2) holds
v' . x = v . x ; :: thesis: ( not M,v |= x1 'in' x2 or M,v' |= x1 'in' x2 )
assume M,v |= x1 'in' x2 ; :: thesis: M,v' |= x1 'in' x2
then A6: v . x1 in v . x2 by ZF_MODEL:13;
( x1 in Free (x1 'in' x2) & x2 in Free (x1 'in' x2) ) by A2, TARSKI:def 2;
then ( v' . x1 = v . x1 & v' . x2 = v . x2 ) by A5;
hence M,v' |= x1 'in' x2 by A6, ZF_MODEL:13; :: thesis: verum

end;

A7: 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 A8: S₁[H] ; :: thesis: S₁[ 'not' H]
let v, v' be Function of VAR ,M; :: thesis: ( ( for x being Variable st x in Free ('not' H) holds
v' . x = v . x ) & M,v |= 'not' H implies M,v' |= 'not' H )
assume A9: for x being Variable st x in Free ('not' H) holds
v' . x = v . x ; :: thesis: ( not M,v |= 'not' H or M,v' |= 'not' H )
assume M,v |= 'not' H ; :: thesis: M,v' |= 'not' H
then A10: not M,v |= H by ZF_MODEL:14;

now

let x be Variable; :: thesis: ( x in Free H implies v . x = v' . x )
assume x in Free H ; :: thesis: v . x = v' . x
then x in Free ('not' H) by Th65;
hence v . x = v' . x by A9; :: thesis: verum

end;

then not M,v' |= H by A8, A10;
hence M,v' |= 'not' H by ZF_MODEL:14; :: thesis: verum

end;

A11: 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 A12: ( S₁[H1] & S₁[H2] ) ; :: thesis: S₁[H1 '&' H2]
A13: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by Th66;
let v, v' be Function of VAR ,M; :: thesis: ( ( for x being Variable st x in Free (H1 '&' H2) holds
v' . x = v . x ) & M,v |= H1 '&' H2 implies M,v' |= H1 '&' H2 )
assume A14: for x being Variable st x in Free (H1 '&' H2) holds
v' . x = v . x ; :: thesis: ( not M,v |= H1 '&' H2 or M,v' |= H1 '&' H2 )
assume M,v |= H1 '&' H2 ; :: thesis: M,v' |= H1 '&' H2
then A15: ( M,v |= H1 & M,v |= H2 ) by ZF_MODEL:15;

now

let x be Variable; :: thesis: ( x in Free H1 implies v' . x = v . x )
assume x in Free H1 ; :: thesis: v' . x = v . x
then x in Free (H1 '&' H2) by A13, XBOOLE_0:def 3;
hence v' . x = v . x by A14; :: thesis: verum

end;

then A16: M,v' |= H1 by A12, A15;

now

let x be Variable; :: thesis: ( x in Free H2 implies v' . x = v . x )
assume x in Free H2 ; :: thesis: v' . x = v . x
then x in Free (H1 '&' H2) by A13, XBOOLE_0:def 3;
hence v' . x = v . x by A14; :: thesis: verum

end;

then M,v' |= H2 by A12, A15;
hence M,v' |= H1 '&' H2 by A16, ZF_MODEL:15; :: thesis: verum

end;

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

proof

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

now

let m be Element of M; :: thesis: M,v' / x1,m |= H
A21: ( M,v / x1,m |= H & Free (All x1,H) = (Free H) \ {x1} ) by A20, Th67, Th80;

now

let x be Variable; :: thesis: ( x in Free H implies (v' / x1,m) . x = (v / x1,m) . x )
assume x in Free H ; :: thesis: (v' / x1,m) . x = (v / x1,m) . x
then ( ( x in Free (All x1,H) & not x in {x1} ) or x in {x1} ) by A21, XBOOLE_0:def 5;
then ( ( v' . x = v . x & x <> x1 ) or x = x1 ) by A19, TARSKI:def 1;
then ( ( (v' / x1,m) . x = v . x & v . x = (v / x1,m) . x ) or ( (v / x1,m) . x = m & (v' / x1,m) . x = m ) ) by FUNCT_7:34, FUNCT_7:130;
hence (v' / x1,m) . x = (v / x1,m) . x ; :: thesis: verum

end;

hence M,v' / x1,m |= H by A18, A21; :: thesis: verum

end;

hence M,v' |= All x1,H by Th80; :: thesis: verum

end;

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