Theorem prid2 4718

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4716 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 4717	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4687	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2832	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2113  Vcvv 3438  {cpr 4580

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 2115  ax-9 2123  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-sn 4579  df-pr 4581

This theorem is referenced by:  opi2  5415  opeluu  5416  opthwiener  5460  dmrnssfld  5921  funopg  6524  fprb  7138  nlim2  8415  2dom  8965  djuss  9830  dfac2b  10039  brdom7disj  10439  brdom6disj  10440  cnelprrecn  11117  mnfxr  11187  seqexw  13938  m1expcl2  14006  hash2prb  14393  pr2pwpr  14400  sadcf  16378  fnpr2ob  17477  setcepi  18010  setc2obas  18016  setc2ohom  18017  cat1  18019  grpss  18882  efgi1  19648  frgpuptinv  19698  dmdprdpr  19978  dprdpr  19979  cnmsgnsubg  21530  m2detleiblem6  22568  m2detleiblem3  22571  m2detleiblem4  22572  m2detleib  22573  indiscld  23033  xpstopnlem1  23751  xpstopnlem2  23753  ehl2eudis  25376  i1f1lem  25644  i1f1  25645  aannenlem2  26291  taylthlem2  26336  taylthlem2OLD  26337  ppiublem2  27168  lgsdir2lem3  27292  sltres  27628  noextendgt  27636  nolesgn2ores  27638  nosepnelem  27645  nosepdmlem  27649  nolt02o  27661  nosupno  27669  nosupbnd1lem3  27676  nosupbnd1  27680  nosupbnd2lem1  27681  noetainflem1  27703  ecgrtg  29005  elntg  29006  usgr2trlncl  29782  usgrwwlks2on  29980  umgrwwlks2on  29981  wlk2v2e  30181  eulerpathpr  30264  ex-br  30455  ex-eprel  30457  s2rnOLD  32975  trsp2cyc  33154  cyc3fv2  33169  constrconj  33851  nn0constr  33867  subfacp1lem3  35325  kur14lem7  35355  ex-sategoelel12  35570  onpsstopbas  36573  onint1  36592  bj-inftyexpidisj  37354  kelac2  43249  omnord1ex  43488  oege2  43491  oenord1ex  43499  oenord1  43500  oaomoencom  43501  oenassex  43502  omcl3g  43518  onno  43616  fvrcllb1d  43878  relexp1idm  43897  corcltrcl  43922  cotrclrcl  43925  clsk1indlem1  44228  mnuprdlem2  44456  mnuprdlem3  44457  mnurndlem1  44464  refsum2cnlem1  45224  limsup10exlem  45958  fourierdlem103  46395  fourierdlem104  46396  ioorrnopn  46491  ioorrnopnxr  46493  stgr1  48149  grlimgrtrilem1  48189  gpgiedgdmellem  48234  gpgvtx1  48242  gpg3kgrtriex  48277  pglem  48279  gpgprismgr4cycllem3  48285  gpgprismgr4cycllem9  48291  grlimedgnedg  48319  zlmodzxzscm  48545  zlmodzxzldeplem3  48690  nn0sumshdiglemB  48808  2arympt  48837  rrx2pyel  48900  rrx2linesl  48931  2sphere0  48938  termc2  49705