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

Theorem prid2 4241
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 𝐵 ∈ V
Assertion
Ref Expression
prid2 𝐵 ∈ {𝐴, 𝐵}

Proof of Theorem prid2
StepHypRef Expression
1 prid2.1 . . 3 𝐵 ∈ V
21prid1 4240 . 2 𝐵 ∈ {𝐵, 𝐴}
3 prcom 4210 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
42, 3eleqtri 2685 1 𝐵 ∈ {𝐴, 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3172  {cpr 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-sn 4125  df-pr 4127
This theorem is referenced by:  prel12  4318  opi2  4859  opeluu  4860  opthwiener  4892  dmrnssfld  5292  funopg  5822  2dom  7892  dfac2  8813  brdom7disj  9211  brdom6disj  9212  cnelprrecn  9885  mnfxr  11783  m1expcl2  12699  hash2prb  13063  pr2pwpr  13066  sadcf  14959  xpsfrnel2  15994  setcepi  16507  grpss  17209  efgi1  17903  frgpuptinv  17953  dmdprdpr  18217  dprdpr  18218  cnmsgnsubg  19687  m2detleiblem6  20193  m2detleiblem3  20196  m2detleiblem4  20197  m2detleib  20198  indiscld  20647  xpstopnlem1  21364  xpstopnlem2  21366  i1f1lem  23179  i1f1  23180  aannenlem2  23805  taylthlem2  23849  ppiublem2  24645  lgsdir2lem3  24769  ecgrtg  25581  elntg  25582  wlkntrl  25858  usgra2wlkspthlem2  25914  constr3lem4  25941  usg2wlkonot  26176  usg2wotspth  26177  eupath  26274  ex-br  26446  ex-eprel  26448  subfacp1lem3  30224  kur14lem7  30254  fprb  30722  sltres  30867  noxp2o  30870  nobndup  30905  onpsstopbas  31405  onint1  31424  bj-inftyexpidisj  32070  kelac2  36449  fvrcllb1d  36802  relexp1idm  36821  corcltrcl  36846  cotrclrcl  36849  clsk1indlem1  37159  refsum2cnlem1  38015  fourierdlem103  38899  fourierdlem104  38900  ioorrnopn  38998  ioorrnopnxr  39000  usgr2trlncl  40961  umgrwwlks2on  41156  1wlk2v2e  41319  eulerpathpr  41403  zlmodzxzscm  41923  zlmodzxzldeplem3  42080  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator