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
|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vz
 |-  z
1 vw
 |-  w
2 1 cv
 |-  w
3 vx
 |-  x
4 3 cv
 |-  x
5 2 4 wceq
 |-  w = x
6 vy
 |-  y
7 6 cv
 |-  y
8 2 7 wceq
 |-  w = y
9 5 8 wo
 |-  ( w = x \/ w = y )
10 0 cv
 |-  z
11 2 10 wcel
 |-  w e. z
12 9 11 wi
 |-  ( ( w = x \/ w = y ) -> w e. z )
13 12 1 wal
 |-  A. w ( ( w = x \/ w = y ) -> w e. z )
14 13 0 wex
 |-  E. z A. w ( ( w = x \/ w = y ) -> w e. z )