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