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, Th128;
then A3: M,v |= (All (x,(H1 => H2))) => (H1 => (All (x,H2))) ;
for m being Element of M holds M,v / (x,m) |= H1 => H2 by A2;
then M,v |= All (x,(H1 => H2)) by Th71;
hence M,v |= H1 => (All (x,H2)) by A3, ZF_MODEL:18; :: thesis: verum