Metamath Proof Explorer


Theorem axextb

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)

Ref Expression
Assertion axextb
|- ( x = y <-> A. z ( z e. x <-> z e. y ) )

Proof

Step Hyp Ref Expression
1 elequ2g
 |-  ( x = y -> A. z ( z e. x <-> z e. y ) )
2 axextg
 |-  ( A. z ( z e. x <-> z e. y ) -> x = y )
3 1 2 impbii
 |-  ( x = y <-> A. z ( z e. x <-> z e. y ) )