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 ABV

Proof

Step Hyp Ref Expression
1 preq2 y=Bxy=xB
2 1 eleq1d y=BxyVxBV
3 zfpair2 xyV
4 2 3 vtoclg BVxBV
5 preq1 x=AxB=AB
6 5 eleq1d x=AxBVABV
7 4 6 syl5ib x=ABVABV
8 7 vtocleg AVBVABV
9 prprc1 ¬AVAB=B
10 snex BV
11 9 10 eqeltrdi ¬AVABV
12 prprc2 ¬BVAB=A
13 snex AV
14 12 13 eqeltrdi ¬BVABV
15 8 11 14 pm2.61nii ABV