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

Theorem prid2 3748
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 3747 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3718 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2368 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   {cpr 3654
This theorem is referenced by:  prel12  3805  opi2  4257  opthwiener  4284  opeluu  4542  dmrnssfld  4954  funopg  5302  2dom  6949  dfac2  7773  brdom7disj  8172  brdom6disj  8173  mnfxr  10472  m1expcl2  11141  sadcf  12660  xpsfrnel2  13483  setcepi  13936  grpss  14519  efgi1  15046  frgpuptinv  15096  dmdprdpr  15300  dprdpr  15301  indiscld  16844  xpstopnlem1  17516  xpstopnlem2  17518  i1f1lem  19060  i1f1  19061  dvfcn  19274  dvnres  19296  dvexp  19318  dvexp3  19341  dvef  19343  dvsincos  19344  dvlipcn  19357  dv11cn  19364  dvply1  19680  aannenlem2  19725  dvtaylp  19765  taylthlem2  19769  pserdvlem2  19820  pige3  19901  dvlog  20014  advlogexp  20018  logtayl  20023  dvcxp1  20098  dvcxp2  20099  dvatan  20247  efrlim  20280  ppiublem2  20458  lgsdir2lem3  20580  logdivsum  20698  log2sumbnd  20709  ex-br  20834  ex-eprel  20836  subfacp1lem3  23728  kur14lem7  23758  eupath  23920  fprb  24200  sltres  24389  noxp2o  24392  nobndup  24425  onpsstopbas  24941  onint1  24960  dvreasin  25026  toplat  25393  pfsubkl  26150  kelac2  27266  cnmsgnsubg  27537  lhe4.4ex1a  27649  expgrowthi  27653  expgrowth  27655  refsum2cnlem1  27811  dvsinexp  27843  constr3lem4  28393
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-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
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-v 2803  df-un 3170  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator