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:35;

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:71; :: 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:34;

hence M,v |= H by A3, A1, ZF_LANG1:71; :: thesis: verum

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:35;

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:71; :: 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:34;

hence M,v |= H by A3, A1, ZF_LANG1:71; :: thesis: verum