Theorem prid2 4722

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  {cpr 4584

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  opi2  5425  opeluu  5426  opthwiener  5470  dmrnssfld  5931  funopg  6534  fprb  7150  nlim2  8427  2dom  8979  djuss  9844  dfac2b  10053  brdom7disj  10453  brdom6disj  10454  cnelprrecn  11131  mnfxr  11201  seqexw  13952  m1expcl2  14020  hash2prb  14407  pr2pwpr  14414  sadcf  16392  fnpr2ob  17491  setcepi  18024  setc2obas  18030  setc2ohom  18031  cat1  18033  grpss  18899  efgi1  19665  frgpuptinv  19715  dmdprdpr  19995  dprdpr  19996  cnmsgnsubg  21547  m2detleiblem6  22585  m2detleiblem3  22588  m2detleiblem4  22589  m2detleib  22590  indiscld  23050  xpstopnlem1  23768  xpstopnlem2  23770  ehl2eudis  25393  i1f1lem  25661  i1f1  25662  aannenlem2  26308  taylthlem2  26353  taylthlem2OLD  26354  ppiublem2  27185  lgsdir2lem3  27309  ltsres  27645  noextendgt  27653  nolesgn2ores  27655  nosepnelem  27662  nosepdmlem  27666  nolt02o  27678  nosupno  27686  nosupbnd1lem3  27693  nosupbnd1  27697  nosupbnd2lem1  27698  noetainflem1  27720  ecgrtg  29072  elntg  29073  usgr2trlncl  29849  usgrwwlks2on  30047  umgrwwlks2on  30048  wlk2v2e  30248  eulerpathpr  30331  ex-br  30522  ex-eprel  30524  s2rnOLD  33041  trsp2cyc  33221  cyc3fv2  33236  esplyfvaln  33755  constrconj  33927  nn0constr  33943  subfacp1lem3  35402  kur14lem7  35432  ex-sategoelel12  35647  onpsstopbas  36650  onint1  36669  bj-inftyexpidisj  37469  kelac2  43426  omnord1ex  43665  oege2  43668  oenord1ex  43676  oenord1  43677  oaomoencom  43678  oenassex  43679  omcl3g  43695  onnoxp  43793  fvrcllb1d  44055  relexp1idm  44074  corcltrcl  44099  cotrclrcl  44102  clsk1indlem1  44405  mnuprdlem2  44633  mnuprdlem3  44634  mnurndlem1  44641  refsum2cnlem1  45401  limsup10exlem  46134  fourierdlem103  46571  fourierdlem104  46572  ioorrnopn  46667  ioorrnopnxr  46669  stgr1  48325  grlimgrtrilem1  48365  gpgiedgdmellem  48410  gpgvtx1  48418  gpg3kgrtriex  48453  pglem  48455  gpgprismgr4cycllem3  48461  gpgprismgr4cycllem9  48467  grlimedgnedg  48495  zlmodzxzscm  48721  zlmodzxzldeplem3  48866  nn0sumshdiglemB  48984  2arympt  49013  rrx2pyel  49076  rrx2linesl  49107  2sphere0  49114  termc2  49881