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

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

now

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

now

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 Th80;
M,v / x,m |= H1 => H2 by A2, Th80;
hence M,v / x,m |= H2 by A4, ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= All x,H2 by Th80; :: 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