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

Theorem prex 4233
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 3751), 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 3720 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2362 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4231 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2856 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3719 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2362 . . . 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 2867 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3749 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4232 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2384 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3750 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4232 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2384 . 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 1632    e. wcel 1696   _Vcvv 2801   {csn 3653   {cpr 3654
This theorem is referenced by:  opex  4253  opi2  4257  opth  4261  opeqsn  4278  opeqpr  4279  opthwiener  4284  uniop  4285  fr2nr  4387  unex  4534  tpex  4535  op1stb  4585  xpsspwOLD  4814  relop  4850  pw2f1olem  6982  1sdom  7081  opthreg  7335  pr2ne  7651  dfac2  7773  intwun  8373  wunex2  8376  wuncval2  8385  intgru  8452  xrex  10367  prmreclem2  12980  prdsval  13371  imasval  13430  isposix  14107  ipoval  14273  spwpr4  14356  frmdval  14489  indistopon  16754  pptbas  16761  indistpsALT  16766  tmslem  18044  sqff1o  20436  dchrval  20489  ex-uni  20829  ex-eprel  20836  prelpwi  23201  prsiga  23507  difelsiga  23509  unelsiga  23510  measssd  23558  indf1ofs  23624  probun  23637  coinflipprob  23695  coinflipspace  23696  coinfliprv  23698  subfacp1lem3  23728  subfacp1lem5  23730  umgra1  23893  vdgr1b  23910  vdgr1a  23912  eupap1  23915  eupath2lem3  23918  eupath2  23919  vdegp1ai  23923  vdegp1bi  23924  altopex  24566  altopthsn  24567  altxpsspw  24583  cbcpcp  25265  nfwpr4c  25388  cntrset  25705  pgapspf  26155  pgapspf2  26156  kelac2lem  27265  kelac2  27266  psgnghm  27540  mendval  27594  prelpw  28184  uslgra1  28252  usgra1  28253  usgraedgrnv  28257  usgraexmpl  28267  wlkntrllem4  28348  wlkntrl  28350  constr3lem1  28391  constr3cyclpe  28409  3v3e3cycl2  28410  frgra2v  28423  frgra3vlem1  28424  frgra3vlem2  28425  tgrpset  31556  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator