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