let H be ZF-formula; :: thesis: ( H is biconditional implies H = (the_left_side_of H) <=> (the_right_side_of H) )
assume A1: H is biconditional ; :: thesis: H = (the_left_side_of H) <=> (the_right_side_of H)
then ex F being ZF-formula st H = (the_left_side_of H) <=> F by Def37;
hence H = (the_left_side_of H) <=> (the_right_side_of H) by A1, Def38; :: thesis: verum