Metamath Proof Explorer

Theorem prex

Description: The Axiom of Pairing using class variables. Theorem 7.13 of Quine p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc ), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993) Avoid ax-nul and shorten proof. (Revised by GG, 6-Mar-2026)

Ref Expression
Assertion prex ⊢ A B ∈ V

Proof

Step Hyp Ref Expression
1 axprg ⊢ ∃ z ∀ w w = A ∨ w = B → w ∈ z
2 1 sepexi ⊢ ∃ z ∀ w w ∈ z ↔ w = A ∨ w = B
3 dfcleq ⊢ z = A B ↔ ∀ w w ∈ z ↔ w ∈ A B
4 vex ⊢ w ∈ V
5 4 elpr ⊢ w ∈ A B ↔ w = A ∨ w = B
6 5 bibi2i ⊢ w ∈ z ↔ w ∈ A B ↔ w ∈ z ↔ w = A ∨ w = B
7 6 albii ⊢ ∀ w w ∈ z ↔ w ∈ A B ↔ ∀ w w ∈ z ↔ w = A ∨ w = B
8 3 7 bitri ⊢ z = A B ↔ ∀ w w ∈ z ↔ w = A ∨ w = B
9 8 exbii ⊢ ∃ z z = A B ↔ ∃ z ∀ w w ∈ z ↔ w = A ∨ w = B
10 2 9 mpbir ⊢ ∃ z z = A B
11 10 issetri ⊢ A B ∈ V