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:32;
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 :: thesis: for v9 being Function of VAR,M st ( for y being Variable st v9 . y <> v . y holds
x = y ) holds
M,v9 |= H

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

end;

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