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

Theorem prid2 3639
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 3638 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3609 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2325 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2727   {cpr 3545
This theorem is referenced by:  prel12  3689  opi2  4134  opthwiener  4161  opeluu  4417  dmrnssfld  4845  funopg  5144  2dom  6818  dfac2  7641  brdom7disj  8040  brdom6disj  8041  mnfxr  10335  m1expcl2  11003  sadcf  12518  xpsfrnel2  13341  setcepi  13764  grpss  14338  efgi1  14865  frgpuptinv  14915  dmdprdpr  15119  dprdpr  15120  indiscld  16660  xpstopnlem1  17332  xpstopnlem2  17334  i1f1lem  18876  i1f1  18877  dvfcn  19090  dvnres  19112  dvexp  19134  dvexp3  19157  dvef  19159  dvsincos  19160  dvlipcn  19173  dv11cn  19180  dvply1  19496  aannenlem2  19541  dvtaylp  19581  taylthlem2  19585  pserdvlem2  19636  pige3  19717  dvlog  19830  advlogexp  19834  logtayl  19839  dvcxp1  19950  dvcxp2  19951  dvatan  20063  efrlim  20096  ppiublem2  20274  lgsdir2lem3  20396  logdivsum  20514  log2sumbnd  20525  ex-br  20631  ex-eprel  20633  subfacp1lem3  22884  kur14lem7  22914  eupath  23076  fprb  23297  sltres  23485  noxp2o  23488  axfelem9  23522  onpsstopbas  24043  onint1  24062  toplat  24456  pfsubkl  25213  kelac2  26329  cnmsgnsubg  26600  lhe4.4ex1a  26712  expgrowthi  26716  expgrowth  26718
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-sn 3550  df-pr 3551
  Copyright terms: Public domain W3C validator