let H1, H2 be ZF-formula; :: thesis: for x being Variable
for M being non empty set st not x in Free H1 holds
M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
let x be Variable; :: thesis: for M being non empty set st not x in Free H1 holds
M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
let M be non empty set ; :: thesis: ( not x in Free H1 implies M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2))) )
assume A1: not x in Free H1 ; :: thesis: M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))

now :: thesis: ( M,v |= All (x,(H1 => H2)) implies M,v |= H1 => (All (x,H2)) )

assume A2: M,v |= All (x,(H1 => H2)) ; :: thesis: M,v |= H1 => (All (x,H2))

now :: thesis: ( M,v |= H1 implies M,v |= All (x,H2) )

assume A3: M,v |= H1 ; :: thesis: M,v |= All (x,H2)

now :: thesis: for m being Element of M holds M,v / (x,m) |= H2

let m be Element of M; :: thesis: M,v / (x,m) |= H2
M,v |= All (x,H1) by A1, A3, ZFMODEL1:10;
then A4: M,v / (x,m) |= H1 by Th71;
M,v / (x,m) |= H1 => H2 by A2, Th71;
hence M,v / (x,m) |= H2 by A4, ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= All (x,H2) by Th71; :: thesis: verum

end;

hence M,v |= H1 => (All (x,H2)) by ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= (All (x,(H1 => H2))) => (H1 => (All (x,H2))) by ZF_MODEL:18; :: thesis: verum