let H1, H2 be ZF-formula; :: thesis: for x being Variable
for M being non empty set st M |= H1 => (All (x,H2)) holds
M |= H1 => H2
let x be Variable; :: thesis: for M being non empty set st M |= H1 => (All (x,H2)) holds
M |= H1 => H2
let M be non empty set ; :: thesis: ( M |= H1 => (All (x,H2)) implies M |= H1 => H2 )
assume A1: for v being Function of VAR,M holds M,v |= H1 => (All (x,H2)) ; :: according to ZF_MODEL:def 5 :: thesis: M |= H1 => H2
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= H1 => H2
A2: M,v |= H1 => (All (x,H2)) by A1;
now :: thesis: ( M,v |= H1 implies M,v |= H2 )
assume M,v |= H1 ; :: thesis: M,v |= H2
then M,v |= All (x,H2) by A2, ZF_MODEL:18;
then M,v / (x,(v . x)) |= H2 by Th71;
hence M,v |= H2 by FUNCT_7:35; :: thesis: verum
end;
hence M,v |= H1 => H2 by ZF_MODEL:18; :: thesis: verum