Theorem prid2 4768

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  opi2  5480  opeluu  5481  opthwiener  5524  dmrnssfld  5987  funopg  6602  fprb  7214  nlim2  8527  2dom  9069  djuss  9958  dfac2b  10169  brdom7disj  10569  brdom6disj  10570  cnelprrecn  11246  mnfxr  11316  seqexw  14055  m1expcl2  14123  hash2prb  14508  pr2pwpr  14515  sadcf  16487  fnpr2ob  17605  setcepi  18142  setc2obas  18148  setc2ohom  18149  cat1  18151  grpss  18985  efgi1  19754  frgpuptinv  19804  dmdprdpr  20084  dprdpr  20085  cnmsgnsubg  21613  m2detleiblem6  22648  m2detleiblem3  22651  m2detleiblem4  22652  m2detleib  22653  indiscld  23115  xpstopnlem1  23833  xpstopnlem2  23835  ehl2eudis  25470  i1f1lem  25738  i1f1  25739  aannenlem2  26386  taylthlem2  26431  taylthlem2OLD  26432  ppiublem2  27262  lgsdir2lem3  27386  sltres  27722  noextendgt  27730  nolesgn2ores  27732  nosepnelem  27739  nosepdmlem  27743  nolt02o  27755  nosupno  27763  nosupbnd1lem3  27770  nosupbnd1  27774  nosupbnd2lem1  27775  noetainflem1  27797  ecgrtg  29013  elntg  29014  usgr2trlncl  29793  umgrwwlks2on  29987  wlk2v2e  30186  eulerpathpr  30269  ex-br  30460  ex-eprel  30462  s2rnOLD  32913  trsp2cyc  33126  cyc3fv2  33141  constrconj  33750  subfacp1lem3  35167  kur14lem7  35197  ex-sategoelel12  35412  onpsstopbas  36413  onint1  36432  bj-inftyexpidisj  37193  kelac2  43054  omnord1ex  43294  oege2  43297  oenord1ex  43305  oenord1  43306  oaomoencom  43307  oenassex  43308  omcl3g  43324  onno  43423  fvrcllb1d  43685  relexp1idm  43704  corcltrcl  43729  cotrclrcl  43732  clsk1indlem1  44035  mnuprdlem2  44269  mnuprdlem3  44270  mnurndlem1  44277  refsum2cnlem1  44975  limsup10exlem  45728  fourierdlem103  46165  fourierdlem104  46166  ioorrnopn  46261  ioorrnopnxr  46263  stgr1  47864  grlimgrtrilem1  47897  gpgedgel  47943  gpgvtx1  47945  zlmodzxzscm  48202  zlmodzxzldeplem3  48348  nn0sumshdiglemB  48470  2arympt  48499  rrx2pyel  48562  rrx2linesl  48593  2sphere0  48600