let H be ZF-formula; for M being non empty set
for v being Function of VAR,M st H is biconditional holds
( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )
let M be non empty set ; for v being Function of VAR,M st H is biconditional holds
( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )
let v be Function of VAR,M; ( H is biconditional implies ( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) ) )
assume
H is biconditional
; ( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )
then
H = (the_left_side_of H) <=> (the_right_side_of H)
by ZF_LANG:49;
hence
( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )
by ZF_MODEL:19; verum