Metamath Proof Explorer

Theorem axprg

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

Ref Expression
Assertion axprg ⊢ ∃ z ∀ w w = A ∨ w = B → w ∈ z

Proof

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