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