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

Axiom ax-pr 5356
Description: The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr 5355 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 setvar 𝑤
2 vx . . . . . 6 setvar 𝑥
31, 2weq 1970 . . . . 5 wff 𝑤 = 𝑥
4 vy . . . . . 6 setvar 𝑦
51, 4weq 1970 . . . . 5 wff 𝑤 = 𝑦
63, 5wo 844 . . . 4 wff (𝑤 = 𝑥𝑤 = 𝑦)
7 vz . . . . 5 setvar 𝑧
81, 7wel 2111 . . . 4 wff 𝑤𝑧
96, 8wi 4 . . 3 wff ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)
109, 1wal 1540 . 2 wff 𝑤((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)
1110, 7wex 1786 1 wff 𝑧𝑤((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)
Colors of variables: wff setvar class
This axiom is referenced by:  zfpair2  5357  el  5361
  Copyright terms: Public domain W3C validator