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

Theorem prid2 4662
 Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4660 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 4661 . 2 𝐵 ∈ {𝐵, 𝐴}
3 prcom 4631 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
42, 3eleqtri 2891 1 𝐵 ∈ {𝐴, 𝐵}
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2112  Vcvv 3444  {cpr 4530 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531 This theorem is referenced by:  opi2  5329  opeluu  5330  opthwiener  5372  dmrnssfld  5810  funopg  6362  fprb  6937  2dom  8569  djuss  9337  dfac2b  9545  brdom7disj  9946  brdom6disj  9947  cnelprrecn  10623  mnfxr  10691  seqexw  13384  m1expcl2  13451  hash2prb  13830  pr2pwpr  13837  sadcf  15795  fnpr2ob  16826  setcepi  17343  grpss  18116  efgi1  18842  frgpuptinv  18892  dmdprdpr  19167  dprdpr  19168  cnmsgnsubg  20269  m2detleiblem6  21234  m2detleiblem3  21237  m2detleiblem4  21238  m2detleib  21239  indiscld  21699  xpstopnlem1  22417  xpstopnlem2  22419  ehl2eudis  24029  i1f1lem  24296  i1f1  24297  aannenlem2  24928  taylthlem2  24972  ppiublem2  25790  lgsdir2lem3  25914  ecgrtg  26780  elntg  26781  usgr2trlncl  27552  umgrwwlks2on  27746  wlk2v2e  27945  eulerpathpr  28028  ex-br  28219  ex-eprel  28221  s2rn  30649  trsp2cyc  30818  cyc3fv2  30833  subfacp1lem3  32537  kur14lem7  32567  ex-sategoelel12  32782  sltres  33277  noextendgt  33285  nolesgn2ores  33287  nosepnelem  33292  nosepdmlem  33295  nolt02o  33307  nosupno  33311  nosupbnd1lem3  33318  nosupbnd1  33322  nosupbnd2lem1  33323  onpsstopbas  33886  onint1  33905  bj-inftyexpidisj  34620  kelac2  39996  fvrcllb1d  40383  relexp1idm  40402  corcltrcl  40427  cotrclrcl  40430  clsk1indlem1  40735  mnuprdlem2  40968  mnuprdlem3  40969  mnurndlem1  40976  refsum2cnlem1  41653  limsup10exlem  42401  fourierdlem103  42838  fourierdlem104  42839  ioorrnopn  42934  ioorrnopnxr  42936  zlmodzxzscm  44746  zlmodzxzldeplem3  44898  nn0sumshdiglemB  45021  2arympt  45050  rrx2pyel  45113  rrx2linesl  45144  2sphere0  45151
 Copyright terms: Public domain W3C validator