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 𝑧𝑤 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vz 𝑧
1 vw 𝑤
2 1 cv 𝑤
3 vx 𝑥
4 3 cv 𝑥
5 2 4 wceq 𝑤 = 𝑥
6 vy 𝑦
7 6 cv 𝑦
8 2 7 wceq 𝑤 = 𝑦
9 5 8 wo ( 𝑤 = 𝑥𝑤 = 𝑦 )
10 0 cv 𝑧
11 2 10 wcel 𝑤𝑧
12 9 11 wi ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 )
13 12 1 wal 𝑤 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 )
14 13 0 wex 𝑧𝑤 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 )