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

Theorem prid2 3736
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 3735 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3706 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2356 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   _Vcvv 2789   {cpr 3642
This theorem is referenced by:  prel12  3790  opi2  4240  opthwiener  4267  opeluu  4525  dmrnssfld  4937  funopg  5252  2dom  6928  dfac2  7752  brdom7disj  8151  brdom6disj  8152  mnfxr  10451  m1expcl2  11119  sadcf  12638  xpsfrnel2  13461  setcepi  13914  grpss  14497  efgi1  15024  frgpuptinv  15074  dmdprdpr  15278  dprdpr  15279  indiscld  16822  xpstopnlem1  17494  xpstopnlem2  17496  i1f1lem  19038  i1f1  19039  dvfcn  19252  dvnres  19274  dvexp  19296  dvexp3  19319  dvef  19321  dvsincos  19322  dvlipcn  19335  dv11cn  19342  dvply1  19658  aannenlem2  19703  dvtaylp  19743  taylthlem2  19747  pserdvlem2  19798  pige3  19879  dvlog  19992  advlogexp  19996  logtayl  20001  dvcxp1  20076  dvcxp2  20077  dvatan  20225  efrlim  20258  ppiublem2  20436  lgsdir2lem3  20558  logdivsum  20676  log2sumbnd  20687  ex-br  20793  ex-eprel  20795  subfacp1lem3  23117  kur14lem7  23147  eupath  23309  fprb  23530  sltres  23718  noxp2o  23721  axfelem9  23755  onpsstopbas  24276  onint1  24295  toplat  24689  pfsubkl  25446  kelac2  26562  cnmsgnsubg  26833  lhe4.4ex1a  26945  expgrowthi  26949  expgrowth  26951  refsum2cnlem1  27107  dvsinexp  27139
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-sn 3647  df-pr 3648
  Copyright terms: Public domain W3C validator