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

Theorem prid2 4330
 Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4328 and ax-mp 5 has one fewer essential step but one more total step.) (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 4329 . 2 𝐵 ∈ {𝐵, 𝐴}
3 prcom 4299 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
42, 3eleqtri 2728 1 𝐵 ∈ {𝐴, 𝐵}
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2030  Vcvv 3231  {cpr 4212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213 This theorem is referenced by:  prel12  4414  opi2  4967  opeluu  4968  opthwiener  5005  dmrnssfld  5416  funopg  5960  2dom  8070  dfac2  8991  brdom7disj  9391  brdom6disj  9392  cnelprrecn  10067  mnfxr  10134  m1expcl2  12922  hash2prb  13292  pr2pwpr  13299  sadcf  15222  xpsfrnel2  16272  setcepi  16785  grpss  17487  efgi1  18180  frgpuptinv  18230  dmdprdpr  18494  dprdpr  18495  cnmsgnsubg  19971  m2detleiblem6  20480  m2detleiblem3  20483  m2detleiblem4  20484  m2detleib  20485  indiscld  20943  xpstopnlem1  21660  xpstopnlem2  21662  i1f1lem  23501  i1f1  23502  aannenlem2  24129  taylthlem2  24173  ppiublem2  24973  lgsdir2lem3  25097  ecgrtg  25908  elntg  25909  usgr2trlncl  26712  umgrwwlks2on  26923  wlk2v2e  27135  eulerpathpr  27218  2clwwlk2clwwlklem2lem2  27329  ex-br  27418  ex-eprel  27420  subfacp1lem3  31290  kur14lem7  31320  fprb  31795  sltres  31940  noextendgt  31948  nolesgn2ores  31950  nosepnelem  31955  nosepdmlem  31958  nolt02o  31970  nosupno  31974  nosupbnd1lem3  31981  nosupbnd1  31985  nosupbnd2lem1  31986  onpsstopbas  32554  onint1  32573  bj-inftyexpidisj  33227  kelac2  37952  fvrcllb1d  38304  relexp1idm  38323  corcltrcl  38348  cotrclrcl  38351  clsk1indlem1  38660  refsum2cnlem1  39510  limsup10exlem  40322  fourierdlem103  40744  fourierdlem104  40745  ioorrnopn  40843  ioorrnopnxr  40845  zlmodzxzscm  42460  zlmodzxzldeplem3  42616  nn0sumshdiglemB  42739
 Copyright terms: Public domain W3C validator