Theorem prid2 4729

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  {cpr 4593

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3921  df-sn 4592  df-pr 4594

This theorem is referenced by:  opi2  5431  opeluu  5432  opthwiener  5476  dmrnssfld  5939  funopg  6552  fprb  7170  nlim2  8456  2dom  9003  djuss  9879  dfac2b  10090  brdom7disj  10490  brdom6disj  10491  cnelprrecn  11167  mnfxr  11237  seqexw  13988  m1expcl2  14056  hash2prb  14443  pr2pwpr  14450  sadcf  16429  fnpr2ob  17527  setcepi  18056  setc2obas  18062  setc2ohom  18063  cat1  18065  grpss  18892  efgi1  19657  frgpuptinv  19707  dmdprdpr  19987  dprdpr  19988  cnmsgnsubg  21492  m2detleiblem6  22519  m2detleiblem3  22522  m2detleiblem4  22523  m2detleib  22524  indiscld  22984  xpstopnlem1  23702  xpstopnlem2  23704  ehl2eudis  25328  i1f1lem  25596  i1f1  25597  aannenlem2  26243  taylthlem2  26288  taylthlem2OLD  26289  ppiublem2  27120  lgsdir2lem3  27244  sltres  27580  noextendgt  27588  nolesgn2ores  27590  nosepnelem  27597  nosepdmlem  27601  nolt02o  27613  nosupno  27621  nosupbnd1lem3  27628  nosupbnd1  27632  nosupbnd2lem1  27633  noetainflem1  27655  ecgrtg  28916  elntg  28917  usgr2trlncl  29696  umgrwwlks2on  29893  wlk2v2e  30092  eulerpathpr  30175  ex-br  30366  ex-eprel  30368  s2rnOLD  32871  trsp2cyc  33086  cyc3fv2  33101  constrconj  33741  nn0constr  33757  subfacp1lem3  35169  kur14lem7  35199  ex-sategoelel12  35414  onpsstopbas  36413  onint1  36432  bj-inftyexpidisj  37193  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  47950  grlimgrtrilem1  47983  gpgiedgdmellem  48027  gpgvtx1  48035  gpg3kgrtriex  48070  pglem  48072  gpgprismgr4cycllem3  48077  gpgprismgr4cycllem9  48083  zlmodzxzscm  48335  zlmodzxzldeplem3  48481  nn0sumshdiglemB  48599  2arympt  48628  rrx2pyel  48691  rrx2linesl  48722  2sphere0  48729  termc2  49497