Theorem prid2 4723

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  {cpr 4587

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 3446  df-un 3916  df-sn 4586  df-pr 4588

This theorem is referenced by:  opi2  5424  opeluu  5425  opthwiener  5469  dmrnssfld  5926  funopg  6534  fprb  7150  nlim2  8431  2dom  8978  djuss  9849  dfac2b  10060  brdom7disj  10460  brdom6disj  10461  cnelprrecn  11137  mnfxr  11207  seqexw  13958  m1expcl2  14026  hash2prb  14413  pr2pwpr  14420  sadcf  16399  fnpr2ob  17497  setcepi  18030  setc2obas  18036  setc2ohom  18037  cat1  18039  grpss  18868  efgi1  19635  frgpuptinv  19685  dmdprdpr  19965  dprdpr  19966  cnmsgnsubg  21519  m2detleiblem6  22546  m2detleiblem3  22549  m2detleiblem4  22550  m2detleib  22551  indiscld  23011  xpstopnlem1  23729  xpstopnlem2  23731  ehl2eudis  25355  i1f1lem  25623  i1f1  25624  aannenlem2  26270  taylthlem2  26315  taylthlem2OLD  26316  ppiublem2  27147  lgsdir2lem3  27271  sltres  27607  noextendgt  27615  nolesgn2ores  27617  nosepnelem  27624  nosepdmlem  27628  nolt02o  27640  nosupno  27648  nosupbnd1lem3  27655  nosupbnd1  27659  nosupbnd2lem1  27660  noetainflem1  27682  ecgrtg  28963  elntg  28964  usgr2trlncl  29740  umgrwwlks2on  29937  wlk2v2e  30136  eulerpathpr  30219  ex-br  30410  ex-eprel  30412  s2rnOLD  32915  trsp2cyc  33095  cyc3fv2  33110  constrconj  33728  nn0constr  33744  subfacp1lem3  35162  kur14lem7  35192  ex-sategoelel12  35407  onpsstopbas  36411  onint1  36430  bj-inftyexpidisj  37191  kelac2  43047  omnord1ex  43286  oege2  43289  oenord1ex  43297  oenord1  43298  oaomoencom  43299  oenassex  43300  omcl3g  43316  onno  43415  fvrcllb1d  43677  relexp1idm  43696  corcltrcl  43721  cotrclrcl  43724  clsk1indlem1  44027  mnuprdlem2  44255  mnuprdlem3  44256  mnurndlem1  44263  refsum2cnlem1  45024  limsup10exlem  45763  fourierdlem103  46200  fourierdlem104  46201  ioorrnopn  46296  ioorrnopnxr  46298  stgr1  47953  grlimgrtrilem1  47986  gpgiedgdmellem  48030  gpgvtx1  48038  gpg3kgrtriex  48073  pglem  48075  gpgprismgr4cycllem3  48080  gpgprismgr4cycllem9  48086  zlmodzxzscm  48338  zlmodzxzldeplem3  48484  nn0sumshdiglemB  48602  2arympt  48631  rrx2pyel  48694  rrx2linesl  48725  2sphere0  48732  termc2  49500