Theorem prid2 4713

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4711 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

Step	Hyp	Ref	Expression
1		prid2.1	. . 3 ⊢ 𝐵 ∈ V
2	1	prid1 4712	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4682	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2829	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2111  Vcvv 3436  {cpr 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576

This theorem is referenced by:  opi2  5407  opeluu  5408  opthwiener  5452  dmrnssfld  5912  funopg  6515  fprb  7128  nlim2  8405  2dom  8952  djuss  9813  dfac2b  10022  brdom7disj  10422  brdom6disj  10423  cnelprrecn  11099  mnfxr  11169  seqexw  13924  m1expcl2  13992  hash2prb  14379  pr2pwpr  14386  sadcf  16364  fnpr2ob  17462  setcepi  17995  setc2obas  18001  setc2ohom  18002  cat1  18004  grpss  18867  efgi1  19633  frgpuptinv  19683  dmdprdpr  19963  dprdpr  19964  cnmsgnsubg  21514  m2detleiblem6  22541  m2detleiblem3  22544  m2detleiblem4  22545  m2detleib  22546  indiscld  23006  xpstopnlem1  23724  xpstopnlem2  23726  ehl2eudis  25349  i1f1lem  25617  i1f1  25618  aannenlem2  26264  taylthlem2  26309  taylthlem2OLD  26310  ppiublem2  27141  lgsdir2lem3  27265  sltres  27601  noextendgt  27609  nolesgn2ores  27611  nosepnelem  27618  nosepdmlem  27622  nolt02o  27634  nosupno  27642  nosupbnd1lem3  27649  nosupbnd1  27653  nosupbnd2lem1  27654  noetainflem1  27676  ecgrtg  28961  elntg  28962  usgr2trlncl  29738  usgrwwlks2on  29936  umgrwwlks2on  29937  wlk2v2e  30137  eulerpathpr  30220  ex-br  30411  ex-eprel  30413  s2rnOLD  32925  trsp2cyc  33092  cyc3fv2  33107  constrconj  33758  nn0constr  33774  subfacp1lem3  35226  kur14lem7  35256  ex-sategoelel12  35471  onpsstopbas  36474  onint1  36493  bj-inftyexpidisj  37254  kelac2  43168  omnord1ex  43407  oege2  43410  oenord1ex  43418  oenord1  43419  oaomoencom  43420  oenassex  43421  omcl3g  43437  onno  43536  fvrcllb1d  43798  relexp1idm  43817  corcltrcl  43842  cotrclrcl  43845  clsk1indlem1  44148  mnuprdlem2  44376  mnuprdlem3  44377  mnurndlem1  44384  refsum2cnlem1  45144  limsup10exlem  45880  fourierdlem103  46317  fourierdlem104  46318  ioorrnopn  46413  ioorrnopnxr  46415  stgr1  48071  grlimgrtrilem1  48111  gpgiedgdmellem  48156  gpgvtx1  48164  gpg3kgrtriex  48199  pglem  48201  gpgprismgr4cycllem3  48207  gpgprismgr4cycllem9  48213  grlimedgnedg  48241  zlmodzxzscm  48467  zlmodzxzldeplem3  48613  nn0sumshdiglemB  48731  2arympt  48760  rrx2pyel  48823  rrx2linesl  48854  2sphere0  48861  termc2  49629