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

Metamath Proof Explorer

Axiom ax-pr

Description: The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006)

Ref Expression
Assertion ax-pr ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 vz setvar z
1 vw setvar w
2 1 cv setvar w
3 vx setvar x
4 3 cv setvar x
5 2 4 wceq wff w = x
6 vy setvar y
7 6 cv setvar y
8 2 7 wceq wff w = y
9 5 8 wo wff w = x ∨ w = y
10 0 cv setvar z
11 2 10 wcel wff w ∈ z
12 9 11 wi wff w = x ∨ w = y → w ∈ z
13 12 1 wal wff ∀ w w = x ∨ w = y → w ∈ z
14 13 0 wex wff ∃ z ∀ w w = x ∨ w = y → w ∈ z