let F, F1, G, 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 Th30;
hence ( F = F1 & G = G1 ) by Th32; :: thesis: verum