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

Metamath Proof Explorer

Theorem zfpair2

Description: Derive the abbreviated version of the Axiom of Pairing from ax-pr . See zfpair for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006)

Ref Expression
Assertion zfpair2 ⊢ x y ∈ V

Proof

Step Hyp Ref Expression
1 ax-pr ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z
2 1 sepexi ⊢ ∃ z ∀ w w ∈ z ↔ w = x ∨ w = y
3 dfcleq ⊢ z = x y ↔ ∀ w w ∈ z ↔ w ∈ x y
4 vex ⊢ w ∈ V
5 4 elpr ⊢ w ∈ x y ↔ w = x ∨ w = y
6 5 bibi2i ⊢ w ∈ z ↔ w ∈ x y ↔ w ∈ z ↔ w = x ∨ w = y
7 6 albii ⊢ ∀ w w ∈ z ↔ w ∈ x y ↔ ∀ w w ∈ z ↔ w = x ∨ w = y
8 3 7 bitri ⊢ z = x y ↔ ∀ w w ∈ z ↔ w = x ∨ w = y
9 8 exbii ⊢ ∃ z z = x y ↔ ∃ z ∀ w w ∈ z ↔ w = x ∨ w = y
10 2 9 mpbir ⊢ ∃ z z = x y
11 10 issetri ⊢ x y ∈ V