Theorem prid2 4707

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  {cpr 4569

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  opi2  5422  opeluu  5423  opthwiener  5468  dmrnssfld  5929  funopg  6532  fprb  7149  nlim2  8425  2dom  8977  djuss  9844  dfac2b  10053  brdom7disj  10453  brdom6disj  10454  cnelprrecn  11131  mnfxr  11202  seqexw  13979  m1expcl2  14047  hash2prb  14434  pr2pwpr  14441  sadcf  16422  fnpr2ob  17522  setcepi  18055  setc2obas  18061  setc2ohom  18062  cat1  18064  grpss  18930  efgi1  19696  frgpuptinv  19746  dmdprdpr  20026  dprdpr  20027  cnmsgnsubg  21557  m2detleiblem6  22591  m2detleiblem3  22594  m2detleiblem4  22595  m2detleib  22596  indiscld  23056  xpstopnlem1  23774  xpstopnlem2  23776  ehl2eudis  25389  i1f1lem  25656  i1f1  25657  aannenlem2  26295  taylthlem2  26339  ppiublem2  27166  lgsdir2lem3  27290  ltsres  27626  noextendgt  27634  nolesgn2ores  27636  nosepnelem  27643  nosepdmlem  27647  nolt02o  27659  nosupno  27667  nosupbnd1lem3  27674  nosupbnd1  27678  nosupbnd2lem1  27679  noetainflem1  27701  ecgrtg  29052  elntg  29053  usgr2trlncl  29828  usgrwwlks2on  30026  umgrwwlks2on  30027  wlk2v2e  30227  eulerpathpr  30310  ex-br  30501  ex-eprel  30503  s2rnOLD  33004  trsp2cyc  33184  cyc3fv2  33199  esplyfvaln  33718  constrconj  33889  nn0constr  33905  subfacp1lem3  35364  kur14lem7  35394  ex-sategoelel12  35609  onpsstopbas  36612  onint1  36631  bj-inftyexpidisj  37524  kelac2  43493  omnord1ex  43732  oege2  43735  oenord1ex  43743  oenord1  43744  oaomoencom  43745  oenassex  43746  omcl3g  43762  onnoxp  43860  fvrcllb1d  44122  relexp1idm  44141  corcltrcl  44166  cotrclrcl  44169  clsk1indlem1  44472  mnuprdlem2  44700  mnuprdlem3  44701  mnurndlem1  44708  refsum2cnlem1  45468  limsup10exlem  46200  fourierdlem103  46637  fourierdlem104  46638  ioorrnopn  46733  ioorrnopnxr  46735  stgr1  48437  grlimgrtrilem1  48477  gpgiedgdmellem  48522  gpgvtx1  48530  gpg3kgrtriex  48565  pglem  48567  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem9  48579  grlimedgnedg  48607  zlmodzxzscm  48833  zlmodzxzldeplem3  48978  nn0sumshdiglemB  49096  2arympt  49125  rrx2pyel  49188  rrx2linesl  49219  2sphere0  49226  termc2  49993