MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prex Unicode version

Theorem prex 4217
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 3738), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
prex  |-  { A ,  B }  e.  _V

Proof of Theorem prex
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq2 3707 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2349 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4215 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2843 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3706 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2349 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6syl5ib 210 . . 3  |-  ( x  =  A  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
87vtocleg 2854 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3736 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4216 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2371 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3737 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4216 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2371 . 2  |-  ( -.  B  e.  _V  ->  { A ,  B }  e.  _V )
158, 11, 14pm2.61nii 158 1  |-  { A ,  B }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684   _Vcvv 2788   {csn 3640   {cpr 3641
This theorem is referenced by:  opex  4237  opi2  4241  opth  4245  opeqsn  4262  opeqpr  4263  opthwiener  4268  uniop  4269  fr2nr  4371  unex  4518  tpex  4519  op1stb  4569  xpsspwOLD  4798  relop  4834  pw2f1olem  6966  1sdom  7065  opthreg  7319  pr2ne  7635  dfac2  7757  intwun  8357  wunex2  8360  wuncval2  8369  intgru  8436  xrex  10351  prmreclem2  12964  prdsval  13355  imasval  13414  isposix  14091  ipoval  14257  spwpr4  14340  frmdval  14473  indistopon  16738  pptbas  16745  indistpsALT  16750  tmslem  18028  sqff1o  20420  dchrval  20473  ex-uni  20813  ex-eprel  20820  subfacp1lem3  23124  subfacp1lem5  23126  umgra1  23289  vdgr1b  23306  vdgr1a  23308  eupap1  23311  eupath2lem3  23314  eupath2  23315  vdegp1ai  23319  vdegp1bi  23320  altopex  23905  altopthsn  23906  altxpsspw  23922  cbcpcp  24574  nfwpr4c  24697  cntrset  25014  pgapspf  25464  pgapspf2  25465  kelac2lem  26574  kelac2  26575  psgnghm  26849  mendval  26903  prelpw  27485  uslgra1  27517  usgra1  27518  usgraexmpl  27530  frgra2v  27539  frgra3vlem1  27540  frgra3vlem2  27541  tgrpset  30307  hlhilset  31500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator