let x be Variable; :: thesis: for M being non empty set
for m being Element of M
for H being ZF-formula
for v being Function of VAR ,M st not x in Free H holds
( M,v |= H iff M,v / x,m |= H )
let M be non empty set ; :: thesis: for m being Element of M
for H being ZF-formula
for v being Function of VAR ,M st not x in Free H holds
( M,v |= H iff M,v / x,m |= H )
let m be Element of M; :: thesis: for H being ZF-formula
for v being Function of VAR ,M st not x in Free H holds
( M,v |= H iff M,v / x,m |= H )
let H be ZF-formula; :: thesis: for v being Function of VAR ,M st not x in Free H holds
( M,v |= H iff M,v / x,m |= H )
let v be Function of VAR ,M; :: thesis: ( not x in Free H implies ( M,v |= H iff M,v / x,m |= H ) )
A1: v / x,(v . x) = v by FUNCT_7:37;
assume A2: not x in Free H ; :: thesis: ( M,v |= H iff M,v / x,m |= H )
then ( M,v |= H implies M,v |= All x,H ) by ZFMODEL1:10;
hence ( M,v |= H implies M,v / x,m |= H ) by ZF_LANG1:80; :: thesis: ( M,v / x,m |= H implies M,v |= H )
assume M,v / x,m |= H ; :: thesis: M,v |= H
then A3: M,v / x,m |= All x,H by A2, ZFMODEL1:10;
(v / x,m) / x,(v . x) = v / x,(v . x) by FUNCT_7:36;
hence M,v |= H by A3, A1, ZF_LANG1:80; :: thesis: verum