Theorem prid2 4715

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-pr 4580

This theorem is referenced by:  opi2  5412  opeluu  5413  opthwiener  5457  dmrnssfld  5915  funopg  6516  fprb  7130  nlim2  8408  2dom  8955  djuss  9816  dfac2b  10025  brdom7disj  10425  brdom6disj  10426  cnelprrecn  11102  mnfxr  11172  seqexw  13924  m1expcl2  13992  hash2prb  14379  pr2pwpr  14386  sadcf  16364  fnpr2ob  17462  setcepi  17995  setc2obas  18001  setc2ohom  18002  cat1  18004  grpss  18833  efgi1  19600  frgpuptinv  19650  dmdprdpr  19930  dprdpr  19931  cnmsgnsubg  21484  m2detleiblem6  22511  m2detleiblem3  22514  m2detleiblem4  22515  m2detleib  22516  indiscld  22976  xpstopnlem1  23694  xpstopnlem2  23696  ehl2eudis  25320  i1f1lem  25588  i1f1  25589  aannenlem2  26235  taylthlem2  26280  taylthlem2OLD  26281  ppiublem2  27112  lgsdir2lem3  27236  sltres  27572  noextendgt  27580  nolesgn2ores  27582  nosepnelem  27589  nosepdmlem  27593  nolt02o  27605  nosupno  27613  nosupbnd1lem3  27620  nosupbnd1  27624  nosupbnd2lem1  27625  noetainflem1  27647  ecgrtg  28928  elntg  28929  usgr2trlncl  29705  umgrwwlks2on  29902  wlk2v2e  30101  eulerpathpr  30184  ex-br  30375  ex-eprel  30377  s2rnOLD  32886  trsp2cyc  33066  cyc3fv2  33081  constrconj  33718  nn0constr  33734  subfacp1lem3  35165  kur14lem7  35195  ex-sategoelel12  35410  onpsstopbas  36414  onint1  36433  bj-inftyexpidisj  37194  kelac2  43048  omnord1ex  43287  oege2  43290  oenord1ex  43298  oenord1  43299  oaomoencom  43300  oenassex  43301  omcl3g  43317  onno  43416  fvrcllb1d  43678  relexp1idm  43697  corcltrcl  43722  cotrclrcl  43725  clsk1indlem1  44028  mnuprdlem2  44256  mnuprdlem3  44257  mnurndlem1  44264  refsum2cnlem1  45025  limsup10exlem  45763  fourierdlem103  46200  fourierdlem104  46201  ioorrnopn  46296  ioorrnopnxr  46298  stgr1  47955  grlimgrtrilem1  47995  gpgiedgdmellem  48040  gpgvtx1  48048  gpg3kgrtriex  48083  pglem  48085  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem9  48097  grlimedgnedg  48125  zlmodzxzscm  48351  zlmodzxzldeplem3  48497  nn0sumshdiglemB  48615  2arympt  48644  rrx2pyel  48707  rrx2linesl  48738  2sphere0  48745  termc2  49513