This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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