let p, q be ZF-formula; :: thesis: ( the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q )
p <=> q is biconditional by ZF_LANG:22;
then p <=> q = (the_left_side_of (p <=> q)) <=> (the_right_side_of (p <=> q)) by ZF_LANG:67;
hence ( the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q ) by ZF_LANG:50; :: thesis: verum