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

Theorem prex 4435
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 3940), 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 3908 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2508 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4433 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 3017 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3907 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2508 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6syl5ib 212 . . 3  |-  ( x  =  A  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
87vtocleg 3028 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3938 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4434 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2530 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3939 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4434 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2530 . 2  |-  ( -.  B  e.  _V  ->  { A ,  B }  e.  _V )
158, 11, 14pm2.61nii 161 1  |-  { A ,  B }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    e. wcel 1727   _Vcvv 2962   {csn 3838   {cpr 3839
This theorem is referenced by:  prelpwi  4440  opex  4456  opi2  4460  opth  4464  opeqsn  4481  opeqpr  4482  opthwiener  4487  uniop  4488  fr2nr  4589  unex  4736  tpex  4737  op1stb  4787  xpsspwOLD  5016  relop  5052  pw2f1olem  7241  1sdom  7340  opthreg  7602  pr2ne  7920  dfac2  8042  intwun  8641  wunex2  8644  wuncval2  8653  intgru  8720  xrex  10640  prmreclem2  13316  prdsval  13709  imasval  13768  isposix  14445  ipoval  14611  spwpr4  14694  frmdval  14827  indistopon  17096  pptbas  17103  indistpsALT  17108  tuslem  18328  tmslem  18543  sqff1o  20996  dchrval  21049  umgra1  21392  uslgra1  21423  usgra1  21424  usgraedgrnv  21428  usgrarnedg  21435  usgraedg4  21437  usgraexmpl  21451  cusgrarn  21499  wlkntrllem2  21591  wlkntrl  21593  constr1trl  21619  1pthon  21622  1pthon2v  21624  constr2wlk  21629  constr2trl  21630  constr2spth  21631  constr2pth  21632  2pthon  21633  2pthon3v  21635  constr3lem1  21663  constr3cyclpe  21681  3v3e3cycl2  21682  vdgr1b  21706  vdgr1a  21708  eupap1  21729  eupath2lem3  21732  eupath2  21733  vdegp1ai  21737  vdegp1bi  21738  ex-uni  21765  ex-eprel  21772  indf1ofs  24454  prsiga  24545  difelsiga  24547  measssd  24600  probun  24708  coinflipprob  24768  coinflipspace  24769  coinfliprv  24771  coinflippv  24772  subfacp1lem3  24899  subfacp1lem5  24901  altopex  25836  altopthsn  25837  altxpsspw  25853  kelac2lem  27177  kelac2  27178  psgnghm  27452  mendval  27506  usgra2adedgwlkon  28379  usg2wlk  28381  usg2wlkon  28382  frgraun  28484  frgra2v  28487  frgra3vlem1  28488  frgra3vlem2  28489  frgrancvvdeqlem3  28519  tgrpset  31640  hlhilset  32833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pr 4432
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-v 2964  df-dif 3309  df-un 3311  df-nul 3614  df-sn 3844  df-pr 3845
  Copyright terms: Public domain W3C validator