Theorem axext2 2335

Description: The Axiom of Extensionality (ax-ext 2334) 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.)

Assertion

Ref	Expression
axext2	⊢ ∃z((z ∈ x ↔ z ∈ y) → x = y)

Distinct variable group:   x,y,z

Proof of Theorem axext2

Step	Hyp	Ref	Expression
1		ax-ext 2334	. 2 ⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
2		19.36v 1896	. 2 ⊢ (∃z((z ∈ x ↔ z ∈ y) → x = y) ↔ (∀z(z ∈ x ↔ z ∈ y) → x = y))
3	1, 2	mpbir 200	1 ⊢ ∃z((z ∈ x ↔ z ∈ y) → x = y)

Syntax hints:   → wi 4   ↔ wb 176  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is referenced by: (None)