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

Theorem prex 4531
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 3984), 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 3952 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2507 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4529 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 3027 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3951 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2507 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6syl5ib 219 . . 3  |-  ( x  =  A  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
87vtocleg 3040 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3982 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4530 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2529 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3983 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4530 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2529 . 2  |-  ( -.  B  e.  _V  ->  { A ,  B }  e.  _V )
158, 11, 14pm2.61nii 166 1  |-  { A ,  B }  e.  _V
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1364    e. wcel 1761   _Vcvv 2970   {csn 3874   {cpr 3876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3328  df-un 3330  df-nul 3635  df-sn 3875  df-pr 3877
This theorem is referenced by:  prelpwi  4536  opex  4553  opi2  4557  op1stb  4559  opth  4563  opeqsn  4584  opeqpr  4585  opthwiener  4590  uniop  4591  fr2nr  4694  xpsspwOLD  4950  relop  4986  unex  6377  tpex  6378  pw2f1olem  7411  1sdom  7511  opthreg  7820  pr2ne  8168  dfac2  8296  intwun  8898  wunex2  8901  wuncval2  8910  intgru  8977  xrex  10984  pr2pwpr  12179  prmreclem2  13974  prdsval  14389  isposix  15123  clatl  15282  ipoval  15320  frmdval  15522  symg2bas  15896  pmtrprfval  15986  pmtrprfvalrn  15987  psgnprfval1  16019  psgnprfval2  16020  psgnghm  17969  psgnco  17972  evpmodpmf1o  17985  mdetralt  18373  m2detleiblem5  18390  m2detleiblem6  18391  m2detleiblem3  18394  m2detleiblem4  18395  m2detleib  18396  indistopon  18564  pptbas  18571  indistpsALT  18576  tuslem  19801  tmslem  20016  sqff1o  22479  dchrval  22532  eengv  23160  umgra1  23195  uslgra1  23226  usgra1  23227  usgraedgrnv  23231  usgrarnedg  23238  usgraedg4  23240  usgraexmpl  23254  cusgrarn  23302  wlkntrllem2  23394  wlkntrl  23396  constr1trl  23422  1pthon  23425  1pthon2v  23427  constr2wlk  23432  constr2trl  23433  constr2spth  23434  constr2pth  23435  2pthon  23436  2pthon3v  23438  constr3lem1  23466  constr3cyclpe  23484  3v3e3cycl2  23485  vdgr1b  23509  vdgr1a  23511  eupap1  23532  eupath2lem3  23535  eupath2  23536  vdegp1ai  23540  vdegp1bi  23541  ex-uni  23568  ex-eprel  23575  indf1ofs  26418  prsiga  26510  difelsiga  26512  measssd  26565  eulerpartlemn  26694  probun  26732  coinflipprob  26792  coinflipspace  26793  coinfliprv  26795  subfacp1lem3  27000  subfacp1lem5  27002  altopex  27920  altopthsn  27921  altxpsspw  27937  kelac2lem  29342  kelac2  29343  mendval  29465  wwlktovfo  30178  usgra2adedgwlkon  30232  usg2wlk  30234  usg2wlkon  30235  frgraun  30513  frgra2v  30516  frgra3vlem1  30517  frgra3vlem2  30518  frgrancvvdeqlem3  30550  mapprop  30660  zlmodzxzlmod  30668  zlmodzxzel  30669  zlmodzxz0  30670  zlmodzxzscm  30671  zlmodzxzadd  30672  isnzr2hash  30691  zlmodzxzldeplem1  30883  zlmodzxzldeplem3  30885  zlmodzxzldeplem4  30886  ldepsnlinclem1  30888  ldepsnlinclem2  30889  ldepsnlinc  30891  bj-elopg  32251  tgrpset  34111  hlhilset  35304
  Copyright terms: Public domain W3C validator