let p, q be ZF-formula; for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q) )
let M be non empty set ; for v being Function of VAR,M holds
( M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q) )
let v be Function of VAR,M; ( M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q) )
hence
M,v |= (p <=> q) => (p => q)
; M |= (p <=> q) => (p => q)
let v be Function of VAR,M; ZF_MODEL:def 5 M,v |= (p <=> q) => (p => q)
thus
M,v |= (p <=> q) => (p => q)
by A1; verum