Description: A bidirectional version of the axiom of extensionality. Although this
theorem looks like a definition of equality, it requires the axiom of
extensionality for its proof under our axiomatization. See the comments
for ax-ext and df-cleq . (Contributed by NM, 14-Nov-2008)