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 syl6eqel ¬ A V A B V
12 prprc2 ¬ B V A B = A
13 snex A V
14 12 13 syl6eqel ¬ B V A B V
15 8 11 14 pm2.61nii A B V