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

Theorem prid2 3877
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 3876 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3846 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2480 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2920   {cpr 3779
This theorem is referenced by:  prel12  3939  opi2  4395  opthwiener  4422  opeluu  4678  dmrnssfld  5092  funopg  5448  2dom  7142  dfac2  7971  brdom7disj  8369  brdom6disj  8370  mnfxr  10674  m1expcl2  11362  sadcf  12924  xpsfrnel2  13749  setcepi  14202  grpss  14785  efgi1  15312  frgpuptinv  15362  dmdprdpr  15566  dprdpr  15567  indiscld  17114  xpstopnlem1  17798  xpstopnlem2  17800  i1f1lem  19538  i1f1  19539  dvfcn  19752  dvnres  19774  dvexp  19796  dvexp3  19819  dvef  19821  dvsincos  19822  dvlipcn  19835  dv11cn  19842  dvply1  20158  aannenlem2  20203  dvtaylp  20243  taylthlem2  20247  pserdvlem2  20301  pige3  20382  dvlog  20499  advlogexp  20503  logtayl  20508  dvcxp1  20583  dvcxp2  20584  dvatan  20732  efrlim  20765  ppiublem2  20944  lgsdir2lem3  21066  logdivsum  21184  log2sumbnd  21195  wlkntrl  21519  constr3lem4  21591  eupath  21660  ex-br  21696  ex-eprel  21698  lgamgulmlem2  24771  subfacp1lem3  24825  kur14lem7  24855  fprb  25347  sltres  25536  noxp2o  25539  nobndup  25572  onpsstopbas  26088  onint1  26107  dvreasin  26183  kelac2  27035  cnmsgnsubg  27306  lhe4.4ex1a  27418  expgrowthi  27422  expgrowth  27424  refsum2cnlem1  27579  dvsinexp  27611  usgra2pthspth  28039  usgra2wlkspthlem2  28041  usg2wlkonot  28084  usg2wotspth  28085
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 2389
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 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-un 3289  df-sn 3784  df-pr 3785
  Copyright terms: Public domain W3C validator