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 ) )