let H be ZF-formula; for x being Variable
for M being non empty set holds M |= (All (x,H)) => H
let x be Variable; for M being non empty set holds M |= (All (x,H)) => H
let M be non empty set ; M |= (All (x,H)) => H
let v be Function of VAR,M; ZF_MODEL:def 5 M,v |= (All (x,H)) => H
( M,v |= All (x,H) implies M,v / (x,(v . x)) |= H )
by Th71;
then
( M,v |= All (x,H) implies M,v |= H )
by FUNCT_7:35;
hence
M,v |= (All (x,H)) => H
by ZF_MODEL:18; verum