let F, G, F1, G1 be ZF-formula; :: thesis: ( F <=> G = F1 <=> G1 implies ( F = F1 & G = G1 ) )
assume F <=> G = F1 <=> G1 ; :: thesis: ( F = F1 & G = G1 )
then F => G = F1 => G1 by Th47;
hence ( F = F1 & G = G1 ) by Th49; :: thesis: verum