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	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )

Metamath Proof Explorer

Axiom ax-pr

Detailed syntax breakdown