let H be ZF-formula; :: thesis: ( H is biconditional implies ( the_left_side_of H = the_antecedent_of (the_left_argument_of H) & the_left_side_of H = the_consequent_of (the_right_argument_of H) ) )
assume H is biconditional ; :: thesis: ( the_left_side_of H = the_antecedent_of (the_left_argument_of H) & the_left_side_of H = the_consequent_of (the_right_argument_of H) )
then H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
then ( the_left_argument_of H = (the_left_side_of H) => (the_right_side_of H) & the_right_argument_of H = (the_right_side_of H) => (the_left_side_of H) ) by Th4;
hence ( the_left_side_of H = the_antecedent_of (the_left_argument_of H) & the_left_side_of H = the_consequent_of (the_right_argument_of H) ) by Th6; :: thesis: verum