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

Theorem prid2 3913
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 3912 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3882 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2508 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2956   {cpr 3815
This theorem is referenced by:  prel12  3975  opi2  4431  opthwiener  4458  opeluu  4715  dmrnssfld  5129  funopg  5485  2dom  7179  dfac2  8011  brdom7disj  8409  brdom6disj  8410  mnfxr  10714  m1expcl2  11403  sadcf  12965  xpsfrnel2  13790  setcepi  14243  grpss  14826  efgi1  15353  frgpuptinv  15403  dmdprdpr  15607  dprdpr  15608  indiscld  17155  xpstopnlem1  17841  xpstopnlem2  17843  i1f1lem  19581  i1f1  19582  dvfcn  19795  dvnres  19817  dvexp  19839  dvexp3  19862  dvef  19864  dvsincos  19865  dvlipcn  19878  dv11cn  19885  dvply1  20201  aannenlem2  20246  dvtaylp  20286  taylthlem2  20290  pserdvlem2  20344  pige3  20425  dvlog  20542  advlogexp  20546  logtayl  20551  dvcxp1  20626  dvcxp2  20627  dvatan  20775  efrlim  20808  ppiublem2  20987  lgsdir2lem3  21109  logdivsum  21227  log2sumbnd  21238  wlkntrl  21562  constr3lem4  21634  eupath  21703  ex-br  21739  ex-eprel  21741  lgamgulmlem2  24814  subfacp1lem3  24868  kur14lem7  24898  fprb  25397  sltres  25619  noxp2o  25622  nobndup  25655  onpsstopbas  26180  onint1  26199  ftc1anclem8  26287  dvreasin  26290  kelac2  27140  cnmsgnsubg  27411  lhe4.4ex1a  27523  expgrowthi  27527  expgrowth  27529  refsum2cnlem1  27684  dvsinexp  27716  usgra2pthspth  28305  usgra2wlkspthlem2  28307  usg2wlkonot  28350  usg2wotspth  28351
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-un 3325  df-sn 3820  df-pr 3821
  Copyright terms: Public domain W3C validator