Theorem prid2 4767

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  {cpr 4630

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631

This theorem is referenced by:  opi2  5469  opeluu  5470  opthwiener  5514  dmrnssfld  5969  funopg  6582  fprb  7197  nlim2  8492  2dom  9032  djuss  9917  dfac2b  10127  brdom7disj  10528  brdom6disj  10529  cnelprrecn  11205  mnfxr  11275  seqexw  13986  m1expcl2  14055  hash2prb  14437  pr2pwpr  14444  sadcf  16398  fnpr2ob  17508  setcepi  18042  setc2obas  18048  setc2ohom  18049  cat1  18051  grpss  18876  efgi1  19630  frgpuptinv  19680  dmdprdpr  19960  dprdpr  19961  cnmsgnsubg  21349  m2detleiblem6  22348  m2detleiblem3  22351  m2detleiblem4  22352  m2detleib  22353  indiscld  22815  xpstopnlem1  23533  xpstopnlem2  23535  ehl2eudis  25163  i1f1lem  25430  i1f1  25431  aannenlem2  26066  taylthlem2  26110  ppiublem2  26930  lgsdir2lem3  27054  sltres  27389  noextendgt  27397  nolesgn2ores  27399  nosepnelem  27406  nosepdmlem  27410  nolt02o  27422  nosupno  27430  nosupbnd1lem3  27437  nosupbnd1  27441  nosupbnd2lem1  27442  noetainflem1  27464  ecgrtg  28496  elntg  28497  usgr2trlncl  29272  umgrwwlks2on  29466  wlk2v2e  29665  eulerpathpr  29748  ex-br  29939  ex-eprel  29941  s2rn  32365  trsp2cyc  32540  cyc3fv2  32555  subfacp1lem3  34459  kur14lem7  34489  ex-sategoelel12  34704  onpsstopbas  35618  onint1  35637  bj-inftyexpidisj  36394  kelac2  42109  omnord1ex  42356  oege2  42359  oenord1ex  42367  oenord1  42368  oaomoencom  42369  oenassex  42370  omcl3g  42386  onno  42486  fvrcllb1d  42748  relexp1idm  42767  corcltrcl  42792  cotrclrcl  42795  clsk1indlem1  43098  mnuprdlem2  43334  mnuprdlem3  43335  mnurndlem1  43342  refsum2cnlem1  44023  limsup10exlem  44787  fourierdlem103  45224  fourierdlem104  45225  ioorrnopn  45320  ioorrnopnxr  45322  zlmodzxzscm  47122  zlmodzxzldeplem3  47271  nn0sumshdiglemB  47394  2arympt  47423  rrx2pyel  47486  rrx2linesl  47517  2sphere0  47524