let H be ZF-formula; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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:67;
hence ( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) ) by ZF_MODEL:19; :: thesis: verum