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

Theorem prid2 3735
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 3734 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3705 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2355 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   {cpr 3641
This theorem is referenced by:  prel12  3789  opi2  4241  opthwiener  4268  opeluu  4526  dmrnssfld  4938  funopg  5286  2dom  6933  dfac2  7757  brdom7disj  8156  brdom6disj  8157  mnfxr  10456  m1expcl2  11125  sadcf  12644  xpsfrnel2  13467  setcepi  13920  grpss  14503  efgi1  15030  frgpuptinv  15080  dmdprdpr  15284  dprdpr  15285  indiscld  16828  xpstopnlem1  17500  xpstopnlem2  17502  i1f1lem  19044  i1f1  19045  dvfcn  19258  dvnres  19280  dvexp  19302  dvexp3  19325  dvef  19327  dvsincos  19328  dvlipcn  19341  dv11cn  19348  dvply1  19664  aannenlem2  19709  dvtaylp  19749  taylthlem2  19753  pserdvlem2  19804  pige3  19885  dvlog  19998  advlogexp  20002  logtayl  20007  dvcxp1  20082  dvcxp2  20083  dvatan  20231  efrlim  20264  ppiublem2  20442  lgsdir2lem3  20564  logdivsum  20682  log2sumbnd  20693  ex-br  20818  ex-eprel  20820  subfacp1lem3  23713  kur14lem7  23743  eupath  23905  fprb  24129  sltres  24318  noxp2o  24321  nobndup  24354  onpsstopbas  24869  onint1  24888  dvreasin  24923  toplat  25290  pfsubkl  26047  kelac2  27163  cnmsgnsubg  27434  lhe4.4ex1a  27546  expgrowthi  27550  expgrowth  27552  refsum2cnlem1  27708  dvsinexp  27740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator