let H be ZF-formula; :: thesis: for x being Variable
for M being non empty set
for v being Function of VAR ,M holds
( M,v |= All x,H iff for m being Element of M holds M,v / x,m |= H )
let x be Variable; :: thesis: for M being non empty set
for v being Function of VAR ,M holds
( M,v |= All x,H iff for m being Element of M holds M,v / x,m |= H )
let M be non empty set ; :: thesis: for v being Function of VAR ,M holds
( M,v |= All x,H iff for m being Element of M holds M,v / x,m |= H )
let v be Function of VAR ,M; :: thesis: ( M,v |= All x,H iff for m being Element of M holds M,v / x,m |= H )
thus ( M,v |= All x,H implies for m being Element of M holds M,v / x,m |= H ) :: thesis: ( ( for m being Element of M holds M,v / x,m |= H ) implies M,v |= All x,H )

proof

assume A1: M,v |= All x,H ; :: thesis: for m being Element of M holds M,v / x,m |= H
let m be Element of M; :: thesis: M,v / x,m |= H
for y being Variable st (v / x,m) . y <> v . y holds
x = y by FUNCT_7:34;
hence M,v / x,m |= H by A1, ZF_MODEL:16; :: thesis: verum

end;

assume A2: for m being Element of M holds M,v / x,m |= H ; :: thesis: M,v |= All x,H

now

let v' be Function of VAR ,M; :: thesis: ( ( for y being Variable st v' . y <> v . y holds
x = y ) implies M,v' |= H )
assume for y being Variable st v' . y <> v . y holds
x = y ; :: thesis: M,v' |= H
then v' = v / x,(v' . x) by FUNCT_7:131;
hence M,v' |= H by A2; :: thesis: verum

end;

hence M,v |= All x,H by ZF_MODEL:16; :: thesis: verum