This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } e. _V

Proof

Step Hyp Ref Expression
1 preq2 
 |-  ( y = B -> { x , y } = { x , B } )
2 1 eleq1d 
 |-  ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3 zfpair2 
 |-  { x , y } e. _V
4 2 3 vtoclg 
 |-  ( B e. _V -> { x , B } e. _V )
5 preq1 
 |-  ( x = A -> { x , B } = { A , B } )
6 5 eleq1d 
 |-  ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7 4 6 imbitrid 
 |-  ( x = A -> ( B e. _V -> { A , B } e. _V ) )
8 7 vtocleg 
 |-  ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9 prprc1 
 |-  ( -. A e. _V -> { A , B } = { B } )
10 snex 
 |-  { B } e. _V
11 9 10 eqeltrdi 
 |-  ( -. A e. _V -> { A , B } e. _V )
12 prprc2 
 |-  ( -. B e. _V -> { A , B } = { A } )
13 snex 
 |-  { A } e. _V
14 12 13 eqeltrdi 
 |-  ( -. B e. _V -> { A , B } e. _V )
15 8 11 14 pm2.61nii 
 |-  { A , B } e. _V