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

Theorem prid2 3873
Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
prid2.1  |-  B  e. 
_V
Assertion
Ref Expression
prid2  |-  B  e. 
{ A ,  B }

Proof of Theorem prid2
StepHypRef Expression
1 prid2.1 . . 3  |-  B  e. 
_V
21prid1 3872 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3842 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2476 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916   {cpr 3775
This theorem is referenced by:  prel12  3935  opi2  4391  opthwiener  4418  opeluu  4674  dmrnssfld  5088  funopg  5444  2dom  7138  dfac2  7967  brdom7disj  8365  brdom6disj  8366  mnfxr  10670  m1expcl2  11358  sadcf  12920  xpsfrnel2  13745  setcepi  14198  grpss  14781  efgi1  15308  frgpuptinv  15358  dmdprdpr  15562  dprdpr  15563  indiscld  17110  xpstopnlem1  17794  xpstopnlem2  17796  i1f1lem  19534  i1f1  19535  dvfcn  19748  dvnres  19770  dvexp  19792  dvexp3  19815  dvef  19817  dvsincos  19818  dvlipcn  19831  dv11cn  19838  dvply1  20154  aannenlem2  20199  dvtaylp  20239  taylthlem2  20243  pserdvlem2  20297  pige3  20378  dvlog  20495  advlogexp  20499  logtayl  20504  dvcxp1  20579  dvcxp2  20580  dvatan  20728  efrlim  20761  ppiublem2  20940  lgsdir2lem3  21062  logdivsum  21180  log2sumbnd  21191  wlkntrl  21515  constr3lem4  21587  eupath  21656  ex-br  21692  ex-eprel  21694  lgamgulmlem2  24767  subfacp1lem3  24821  kur14lem7  24851  fprb  25343  sltres  25532  noxp2o  25535  nobndup  25568  onpsstopbas  26084  onint1  26103  dvreasin  26179  kelac2  27031  cnmsgnsubg  27302  lhe4.4ex1a  27414  expgrowthi  27418  expgrowth  27420  refsum2cnlem1  27575  dvsinexp  27607  usgra2pthspth  28035  usgra2wlkspthlem2  28037  usg2wlkonot  28080  usg2wotspth  28081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-sn 3780  df-pr 3781
  Copyright terms: Public domain W3C validator