Theorem axprg

Description: Derive The Axiom of Pairing with class variables. (Contributed by GG, 6-Mar-2026)

	Ref	Expression
Assertion	axprg	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝐴 ↔ 𝑥 = 𝐴 ) )
2		eqeq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝐵 ↔ 𝑥 = 𝐵 ) )
3	1 2	orbi12d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
4	3	cbvexvw	⊢ ( ∃ 𝑤 ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
5		axprglem	⊢ ( 𝑥 = 𝐴 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
6		axprglem	⊢ ( 𝑥 = 𝐵 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐵 ∨ 𝑤 = 𝐴 ) → 𝑤 ∈ 𝑧 ) )
7		pm1.4	⊢ ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( 𝑤 = 𝐵 ∨ 𝑤 = 𝐴 ) )
8	7	imim1i	⊢ ( ( ( 𝑤 = 𝐵 ∨ 𝑤 = 𝐴 ) → 𝑤 ∈ 𝑧 ) → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
9	8	alimi	⊢ ( ∀ 𝑤 ( ( 𝑤 = 𝐵 ∨ 𝑤 = 𝐴 ) → 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
10	9	eximi	⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐵 ∨ 𝑤 = 𝐴 ) → 𝑤 ∈ 𝑧 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
11	6 10	syl	⊢ ( 𝑥 = 𝐵 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
12	5 11	jaoi	⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
13	12	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
14	4 13	sylbi	⊢ ( ∃ 𝑤 ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
15		alnex	⊢ ( ∀ 𝑤 ¬ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) ↔ ¬ ∃ 𝑤 ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) )
16		pm2.21	⊢ ( ¬ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
17	16	alimi	⊢ ( ∀ 𝑤 ¬ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
18	15 17	sylbir	⊢ ( ¬ ∃ 𝑤 ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
19	18	exgen	⊢ ∃ 𝑧 ( ¬ ∃ 𝑤 ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
20	19	19.37iv	⊢ ( ¬ ∃ 𝑤 ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
21	14 20	pm2.61i	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 )