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

Theorem prid2 3858
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 3857 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3827 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2461 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   _Vcvv 2901   {cpr 3760
This theorem is referenced by:  prel12  3919  opi2  4374  opthwiener  4401  opeluu  4657  dmrnssfld  5071  funopg  5427  2dom  7117  dfac2  7946  brdom7disj  8344  brdom6disj  8345  mnfxr  10648  m1expcl2  11332  sadcf  12894  xpsfrnel2  13719  setcepi  14172  grpss  14755  efgi1  15282  frgpuptinv  15332  dmdprdpr  15536  dprdpr  15537  indiscld  17080  xpstopnlem1  17764  xpstopnlem2  17766  i1f1lem  19450  i1f1  19451  dvfcn  19664  dvnres  19686  dvexp  19708  dvexp3  19731  dvef  19733  dvsincos  19734  dvlipcn  19747  dv11cn  19754  dvply1  20070  aannenlem2  20115  dvtaylp  20155  taylthlem2  20159  pserdvlem2  20213  pige3  20294  dvlog  20411  advlogexp  20415  logtayl  20420  dvcxp1  20495  dvcxp2  20496  dvatan  20644  efrlim  20677  ppiublem2  20856  lgsdir2lem3  20978  logdivsum  21096  log2sumbnd  21107  constr3lem4  21484  eupath  21553  ex-br  21589  ex-eprel  21591  lgamgulmlem2  24595  subfacp1lem3  24649  kur14lem7  24679  fprb  25155  sltres  25344  noxp2o  25347  nobndup  25380  onpsstopbas  25896  onint1  25915  dvreasin  25982  kelac2  26834  cnmsgnsubg  27105  lhe4.4ex1a  27217  expgrowthi  27221  expgrowth  27223  refsum2cnlem1  27378  dvsinexp  27410
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
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 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-un 3270  df-sn 3765  df-pr 3766
  Copyright terms: Public domain W3C validator