This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ax-ext	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
2		19.36v	⊢ ( ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
3	1 2	mpbir	⊢ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )