MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-pr Unicode version

Axiom ax-pr 4442
Description: The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 4441 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.)
Assertion
Ref Expression
ax-pr
Distinct variable groups:   , ,   , ,

Detailed syntax breakdown of Axiom ax-pr
StepHypRef Expression
1 vw . . . . . 6
2 vx . . . . . 6
31, 2weq 1655 . . . . 5
4 vy . . . . . 6
51, 4weq 1655 . . . . 5
63, 5wo 359 . . . 4
7 vz . . . . 5
81, 7wel 1729 . . . 4
96, 8wi 4 . . 3
109, 1wal 1550 . 2
1110, 7wex 1551 1
Colors of variables: wff set class
This axiom is referenced by:  zfpair2  4443
  Copyright terms: Public domain W3C validator