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

Theorem prex 4398
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 3908), 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 3876 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2501 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4396 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 3003 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3875 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2501 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6syl5ib 211 . . 3  |-  ( x  =  A  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
87vtocleg 3014 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3906 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4397 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2523 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3907 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4397 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2523 . 2  |-  ( -.  B  e.  _V  ->  { A ,  B }  e.  _V )
158, 11, 14pm2.61nii 160 1  |-  { A ,  B }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    e. wcel 1725   _Vcvv 2948   {csn 3806   {cpr 3807
This theorem is referenced by:  prelpwi  4403  opex  4419  opi2  4423  opth  4427  opeqsn  4444  opeqpr  4445  opthwiener  4450  uniop  4451  fr2nr  4552  unex  4698  tpex  4699  op1stb  4749  xpsspwOLD  4978  relop  5014  pw2f1olem  7203  1sdom  7302  opthreg  7562  pr2ne  7878  dfac2  8000  intwun  8599  wunex2  8602  wuncval2  8611  intgru  8678  xrex  10598  prmreclem2  13273  prdsval  13666  imasval  13725  isposix  14402  ipoval  14568  spwpr4  14651  frmdval  14784  indistopon  17053  pptbas  17060  indistpsALT  17065  tuslem  18285  tmslem  18500  sqff1o  20953  dchrval  21006  umgra1  21349  uslgra1  21380  usgra1  21381  usgraedgrnv  21385  usgrarnedg  21392  usgraedg4  21394  usgraexmpl  21408  cusgrarn  21456  wlkntrllem2  21548  wlkntrl  21550  constr1trl  21576  1pthon  21579  1pthon2v  21581  constr2wlk  21586  constr2trl  21587  constr2spth  21588  constr2pth  21589  2pthon  21590  2pthon3v  21592  constr3lem1  21620  constr3cyclpe  21638  3v3e3cycl2  21639  vdgr1b  21663  vdgr1a  21665  eupap1  21686  eupath2lem3  21689  eupath2  21690  vdegp1ai  21694  vdegp1bi  21695  ex-uni  21722  ex-eprel  21729  indf1ofs  24411  prsiga  24502  difelsiga  24504  measssd  24557  probun  24665  coinflipprob  24725  coinflipspace  24726  coinfliprv  24728  coinflippv  24729  subfacp1lem3  24856  subfacp1lem5  24858  altopex  25753  altopthsn  25754  altxpsspw  25770  kelac2lem  27077  kelac2  27078  psgnghm  27352  mendval  27406  usgra2adedgwlkon  28191  usg2wlk  28193  usg2wlkon  28194  frgraun  28244  frgra2v  28247  frgra3vlem1  28248  frgra3vlem2  28249  frgrancvvdeqlem3  28279  tgrpset  31381  hlhilset  32574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-un 3317  df-nul 3621  df-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator