Theorem axext2 2591

Description: The Axiom of Extensionality (ax-ext 2590) restated so that it postulates the existence of a set 𝑧 given two arbitrary sets 𝑥 and 𝑦. 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.)

Assertion

Ref	Expression
axext2	⊢ ∃𝑧((𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)

Distinct variable group:   𝑥,𝑦,𝑧

Proof of Theorem axext2

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

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by: (None)