let H1, H2 be ZF-formula; :: thesis: for x being Variable
for M being non empty set st not x in Free H1 & M |= H1 => H2 holds
M |= H1 => (All x,H2)
let x be Variable; :: thesis: for M being non empty set st not x in Free H1 & M |= H1 => H2 holds
M |= H1 => (All x,H2)
let M be non empty set ; :: thesis: ( not x in Free H1 & M |= H1 => H2 implies M |= H1 => (All x,H2) )
assume that
A1: not x in Free H1 and
A2: for v being Function of VAR ,M holds M,v |= H1 => H2 ; :: according to ZF_MODEL:def 5 :: thesis: M |= H1 => (All x,H2)
let v be Function of VAR ,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= H1 => (All x,H2)
M |= (All x,(H1 => H2)) => (H1 => (All x,H2)) by A1, Th140;
then A3: M,v |= (All x,(H1 => H2)) => (H1 => (All x,H2)) by ZF_MODEL:def 5;
for m being Element of M holds M,v / x,m |= H1 => H2 by A2;
then M,v |= All x,(H1 => H2) by Th80;
hence M,v |= H1 => (All x,H2) by A3, ZF_MODEL:18; :: thesis: verum