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

Theorem prid2 4724
Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4722 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 4723 . 2 𝐵 ∈ {𝐵, 𝐴}
3 prcom 4693 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
42, 3eleqtri 2836 1 𝐵 ∈ {𝐴, 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3445  {cpr 4588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-un 3915  df-sn 4587  df-pr 4589
This theorem is referenced by:  opi2  5426  opeluu  5427  opthwiener  5471  dmrnssfld  5925  funopg  6535  fprb  7143  nlim2  8436  2dom  8974  djuss  9856  dfac2b  10066  brdom7disj  10467  brdom6disj  10468  cnelprrecn  11144  mnfxr  11212  seqexw  13922  m1expcl2  13991  hash2prb  14371  pr2pwpr  14378  sadcf  16333  fnpr2ob  17440  setcepi  17974  setc2obas  17980  setc2ohom  17981  cat1  17983  grpss  18768  efgi1  19503  frgpuptinv  19553  dmdprdpr  19828  dprdpr  19829  cnmsgnsubg  20981  m2detleiblem6  21975  m2detleiblem3  21978  m2detleiblem4  21979  m2detleib  21980  indiscld  22442  xpstopnlem1  23160  xpstopnlem2  23162  ehl2eudis  24786  i1f1lem  25053  i1f1  25054  aannenlem2  25689  taylthlem2  25733  ppiublem2  26551  lgsdir2lem3  26675  sltres  27010  noextendgt  27018  nolesgn2ores  27020  nosepnelem  27027  nosepdmlem  27031  nolt02o  27043  nosupno  27051  nosupbnd1lem3  27058  nosupbnd1  27062  nosupbnd2lem1  27063  noetainflem1  27085  ecgrtg  27932  elntg  27933  usgr2trlncl  28708  umgrwwlks2on  28902  wlk2v2e  29101  eulerpathpr  29184  ex-br  29375  ex-eprel  29377  s2rn  31800  trsp2cyc  31972  cyc3fv2  31987  subfacp1lem3  33776  kur14lem7  33806  ex-sategoelel12  34021  onpsstopbas  34902  onint1  34921  bj-inftyexpidisj  35681  kelac2  41378  omnord1ex  41624  oege2  41627  oenord1ex  41635  oenord1  41636  oaomoencom  41637  oenassex  41638  omcl3g  41653  onno  41695  fvrcllb1d  41957  relexp1idm  41976  corcltrcl  42001  cotrclrcl  42004  clsk1indlem1  42307  mnuprdlem2  42543  mnuprdlem3  42544  mnurndlem1  42551  refsum2cnlem1  43232  limsup10exlem  44003  fourierdlem103  44440  fourierdlem104  44441  ioorrnopn  44536  ioorrnopnxr  44538  zlmodzxzscm  46423  zlmodzxzldeplem3  46573  nn0sumshdiglemB  46696  2arympt  46725  rrx2pyel  46788  rrx2linesl  46819  2sphere0  46826
  Copyright terms: Public domain W3C validator