let x be Variable; 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 ; 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; 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; 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; ( 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; verum