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

Theorem prid2 3709
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 3708 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3679 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2330 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2763   {cpr 3615
This theorem is referenced by:  prel12  3763  opi2  4213  opthwiener  4240  opeluu  4498  dmrnssfld  4926  funopg  5225  2dom  6901  dfac2  7725  brdom7disj  8124  brdom6disj  8125  mnfxr  10423  m1expcl2  11091  sadcf  12606  xpsfrnel2  13429  setcepi  13882  grpss  14465  efgi1  14992  frgpuptinv  15042  dmdprdpr  15246  dprdpr  15247  indiscld  16790  xpstopnlem1  17462  xpstopnlem2  17464  i1f1lem  19006  i1f1  19007  dvfcn  19220  dvnres  19242  dvexp  19264  dvexp3  19287  dvef  19289  dvsincos  19290  dvlipcn  19303  dv11cn  19310  dvply1  19626  aannenlem2  19671  dvtaylp  19711  taylthlem2  19715  pserdvlem2  19766  pige3  19847  dvlog  19960  advlogexp  19964  logtayl  19969  dvcxp1  20044  dvcxp2  20045  dvatan  20193  efrlim  20226  ppiublem2  20404  lgsdir2lem3  20526  logdivsum  20644  log2sumbnd  20655  ex-br  20761  ex-eprel  20763  subfacp1lem3  23085  kur14lem7  23115  eupath  23277  fprb  23498  sltres  23686  noxp2o  23689  axfelem9  23723  onpsstopbas  24244  onint1  24263  toplat  24657  pfsubkl  25414  kelac2  26530  cnmsgnsubg  26801  lhe4.4ex1a  26913  expgrowthi  26917  expgrowth  26919  refsum2cnlem1  27076
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-un 3132  df-sn 3620  df-pr 3621
  Copyright terms: Public domain W3C validator