Theorem prid2 4744

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

Syntax hints:   ∈ wcel 2109  Vcvv 3464  {cpr 4608

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by:  opi2  5449  opeluu  5450  opthwiener  5494  dmrnssfld  5958  funopg  6575  fprb  7191  nlim2  8507  2dom  9049  djuss  9939  dfac2b  10150  brdom7disj  10550  brdom6disj  10551  cnelprrecn  11227  mnfxr  11297  seqexw  14040  m1expcl2  14108  hash2prb  14495  pr2pwpr  14502  sadcf  16477  fnpr2ob  17577  setcepi  18106  setc2obas  18112  setc2ohom  18113  cat1  18115  grpss  18942  efgi1  19707  frgpuptinv  19757  dmdprdpr  20037  dprdpr  20038  cnmsgnsubg  21542  m2detleiblem6  22569  m2detleiblem3  22572  m2detleiblem4  22573  m2detleib  22574  indiscld  23034  xpstopnlem1  23752  xpstopnlem2  23754  ehl2eudis  25379  i1f1lem  25647  i1f1  25648  aannenlem2  26294  taylthlem2  26339  taylthlem2OLD  26340  ppiublem2  27171  lgsdir2lem3  27295  sltres  27631  noextendgt  27639  nolesgn2ores  27641  nosepnelem  27648  nosepdmlem  27652  nolt02o  27664  nosupno  27672  nosupbnd1lem3  27679  nosupbnd1  27683  nosupbnd2lem1  27684  noetainflem1  27706  ecgrtg  28967  elntg  28968  usgr2trlncl  29747  umgrwwlks2on  29944  wlk2v2e  30143  eulerpathpr  30226  ex-br  30417  ex-eprel  30419  s2rnOLD  32924  trsp2cyc  33139  cyc3fv2  33154  constrconj  33784  nn0constr  33800  subfacp1lem3  35209  kur14lem7  35239  ex-sategoelel12  35454  onpsstopbas  36453  onint1  36472  bj-inftyexpidisj  37233  kelac2  43064  omnord1ex  43303  oege2  43306  oenord1ex  43314  oenord1  43315  oaomoencom  43316  oenassex  43317  omcl3g  43333  onno  43432  fvrcllb1d  43694  relexp1idm  43713  corcltrcl  43738  cotrclrcl  43741  clsk1indlem1  44044  mnuprdlem2  44272  mnuprdlem3  44273  mnurndlem1  44280  refsum2cnlem1  45041  limsup10exlem  45781  fourierdlem103  46218  fourierdlem104  46219  ioorrnopn  46314  ioorrnopnxr  46316  stgr1  47953  grlimgrtrilem1  47986  gpgiedgdmellem  48030  gpgvtx1  48038  gpg3kgrtriex  48071  gpgprismgr4cycllem3  48076  gpgprismgr4cycllem9  48082  zlmodzxzscm  48312  zlmodzxzldeplem3  48458  nn0sumshdiglemB  48580  2arympt  48609  rrx2pyel  48672  rrx2linesl  48703  2sphere0  48710  termc2  49383