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 variables_in 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 variables_in 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 variables_in 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 variables_in H holds

( M,v |= H iff M,v / (x,m) |= H )

let v be Function of VAR,M; :: thesis: ( not x in variables_in H implies ( M,v |= H iff M,v / (x,m) |= H ) )

A1: ( M,v / (x,m) |= All (x,H) implies M,(v / (x,m)) / (x,(v . x)) |= H ) by ZF_LANG1:71;

A2: (v / (x,m)) / (x,(v . x)) = v / (x,(v . x)) by FUNCT_7:34;

( M,v |= All (x,H) implies M,v / (x,m) |= H ) by ZF_LANG1:71;

hence ( not x in variables_in H implies ( M,v |= H iff M,v / (x,m) |= H ) ) by A1, A2, Th4, FUNCT_7:35; :: thesis: verum

for m being Element of M

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in 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 variables_in 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 variables_in 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 variables_in H holds

( M,v |= H iff M,v / (x,m) |= H )

let v be Function of VAR,M; :: thesis: ( not x in variables_in H implies ( M,v |= H iff M,v / (x,m) |= H ) )

A1: ( M,v / (x,m) |= All (x,H) implies M,(v / (x,m)) / (x,(v . x)) |= H ) by ZF_LANG1:71;

A2: (v / (x,m)) / (x,(v . x)) = v / (x,(v . x)) by FUNCT_7:34;

( M,v |= All (x,H) implies M,v / (x,m) |= H ) by ZF_LANG1:71;

hence ( not x in variables_in H implies ( M,v |= H iff M,v / (x,m) |= H ) ) by A1, A2, Th4, FUNCT_7:35; :: thesis: verum