Theorem axext 1086

Description: The Axiom of Extensionality (ax-ext 1074) restated so that it postulates the existence of a set z given two arbitrary sets x and y. This way of expressing it follows the general idea of the other ZFC axioms, which is to postulate the existence of sets given other sets.

Assertion

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

Distinct variable group(s):   x,y,z

Proof of Theorem axext

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

Syntax hints:   → wi 2   ↔ wb 127  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org