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)

Ref Expression
Assertion prex ⊢ A B ∈ V

Proof

Step Hyp Ref Expression
1 preq2 ⊢ y = B → x y = x B
2 1 eleq1d ⊢ y = B → x y ∈ V ↔ x B ∈ V
3 zfpair2 ⊢ x y ∈ V
4 2 3 vtoclg ⊢ B ∈ V → x B ∈ V
5 preq1 ⊢ x = A → x B = A B
6 5 eleq1d ⊢ x = A → x B ∈ V ↔ A B ∈ V
7 4 6 syl5ib ⊢ x = A → B ∈ V → A B ∈ V
8 7 vtocleg ⊢ A ∈ V → B ∈ V → A B ∈ V
9 prprc1 ⊢ ¬ A ∈ V → A B = B
10 snex ⊢ B ∈ V
11 9 10 eqeltrdi ⊢ ¬ A ∈ V → A B ∈ V
12 prprc2 ⊢ ¬ B ∈ V → A B = A
13 snex ⊢ A ∈ V
14 12 13 eqeltrdi ⊢ ¬ B ∈ V → A B ∈ V
15 8 11 14 pm2.61nii ⊢ A B ∈ V