Theorem axexte

Description: The axiom of extensionality ( ax-ext ) restated so that it postulates the existence of a set z given two arbitrary sets x and y . This way to express it follows the general idea of the other ZFC axioms, which is to postulate the existence of sets given other sets. (Contributed by NM, 28-Sep-2003)

	Ref	Expression
Assertion	axexte	|- E. z ( ( z e. x <-> z e. y ) -> x = y )

Proof

Step	Hyp	Ref	Expression
1		ax-ext	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
2		19.36v	|- ( E. z ( ( z e. x <-> z e. y ) -> x = y ) <-> ( A. z ( z e. x <-> z e. y ) -> x = y ) )
3	1 2	mpbir	|- E. z ( ( z e. x <-> z e. y ) -> x = y )