Theorem prid2 4720

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  {cpr 4582

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  opi2  5417  opeluu  5418  opthwiener  5462  dmrnssfld  5923  funopg  6526  fprb  7140  nlim2  8417  2dom  8967  djuss  9832  dfac2b  10041  brdom7disj  10441  brdom6disj  10442  cnelprrecn  11119  mnfxr  11189  seqexw  13940  m1expcl2  14008  hash2prb  14395  pr2pwpr  14402  sadcf  16380  fnpr2ob  17479  setcepi  18012  setc2obas  18018  setc2ohom  18019  cat1  18021  grpss  18884  efgi1  19650  frgpuptinv  19700  dmdprdpr  19980  dprdpr  19981  cnmsgnsubg  21532  m2detleiblem6  22570  m2detleiblem3  22573  m2detleiblem4  22574  m2detleib  22575  indiscld  23035  xpstopnlem1  23753  xpstopnlem2  23755  ehl2eudis  25378  i1f1lem  25646  i1f1  25647  aannenlem2  26293  taylthlem2  26338  taylthlem2OLD  26339  ppiublem2  27170  lgsdir2lem3  27294  ltsres  27630  noextendgt  27638  nolesgn2ores  27640  nosepnelem  27647  nosepdmlem  27651  nolt02o  27663  nosupno  27671  nosupbnd1lem3  27678  nosupbnd1  27682  nosupbnd2lem1  27683  noetainflem1  27705  ecgrtg  29056  elntg  29057  usgr2trlncl  29833  usgrwwlks2on  30031  umgrwwlks2on  30032  wlk2v2e  30232  eulerpathpr  30315  ex-br  30506  ex-eprel  30508  s2rnOLD  33026  trsp2cyc  33205  cyc3fv2  33220  constrconj  33902  nn0constr  33918  subfacp1lem3  35376  kur14lem7  35406  ex-sategoelel12  35621  onpsstopbas  36624  onint1  36643  bj-inftyexpidisj  37415  kelac2  43307  omnord1ex  43546  oege2  43549  oenord1ex  43557  oenord1  43558  oaomoencom  43559  oenassex  43560  omcl3g  43576  onnoxp  43674  fvrcllb1d  43936  relexp1idm  43955  corcltrcl  43980  cotrclrcl  43983  clsk1indlem1  44286  mnuprdlem2  44514  mnuprdlem3  44515  mnurndlem1  44522  refsum2cnlem1  45282  limsup10exlem  46016  fourierdlem103  46453  fourierdlem104  46454  ioorrnopn  46549  ioorrnopnxr  46551  stgr1  48207  grlimgrtrilem1  48247  gpgiedgdmellem  48292  gpgvtx1  48300  gpg3kgrtriex  48335  pglem  48337  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem9  48349  grlimedgnedg  48377  zlmodzxzscm  48603  zlmodzxzldeplem3  48748  nn0sumshdiglemB  48866  2arympt  48895  rrx2pyel  48958  rrx2linesl  48989  2sphere0  48996  termc2  49763