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

proof

let v be Function of VAR,M; :: thesis: for m being Element of M st M,v |= All (x,H) holds
M,v / (x,m) |= All (x,H)
let m be Element of M; :: thesis: ( M,v |= All (x,H) implies M,v / (x,m) |= All (x,H) )
assume A2: M,v |= All (x,H) ; :: thesis: M,v / (x,m) |= All (x,H)

now :: thesis: for m9 being Element of M holds M,(v / (x,m)) / (x,m9) |= H

let m9 be Element of M; :: thesis: M,(v / (x,m)) / (x,m9) |= H
(v / (x,m)) / (x,m9) = v / (x,m9) by FUNCT_7:34;
hence M,(v / (x,m)) / (x,m9) |= H by A2, Th71; :: thesis: verum

end;

hence M,v / (x,m) |= All (x,H) by Th71; :: thesis: verum

end;

(v / (x,m)) / (x,(v . x)) = v / (x,(v . x)) by FUNCT_7:34
.= v by FUNCT_7:35 ;
hence ( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) ) by A1; :: thesis: verum