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

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:36;
hence M,(v / x,m) / x,m9 |= H by A2, Th80; :: thesis: verum

end;

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

end;

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