let H be ZF-formula; :: thesis: for x, y being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,H) )
let x, y be Variable; :: thesis: for M being non empty set holds
( M |= H iff M |= All (x,y,H) )
let M be non empty set ; :: thesis: ( M |= H iff M |= All (x,y,H) )
( M |= H iff M |= All (y,H) ) by ZF_MODEL:23;
hence ( M |= H iff M |= All (x,y,H) ) by ZF_MODEL:23; :: thesis: verum