Theorem prid2 4708

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  {cpr 4570

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 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  opi2  5418  opeluu  5419  opthwiener  5463  dmrnssfld  5924  funopg  6527  fprb  7143  nlim2  8419  2dom  8971  djuss  9838  dfac2b  10047  brdom7disj  10447  brdom6disj  10448  cnelprrecn  11125  mnfxr  11196  seqexw  13973  m1expcl2  14041  hash2prb  14428  pr2pwpr  14435  sadcf  16416  fnpr2ob  17516  setcepi  18049  setc2obas  18055  setc2ohom  18056  cat1  18058  grpss  18924  efgi1  19690  frgpuptinv  19740  dmdprdpr  20020  dprdpr  20021  cnmsgnsubg  21570  m2detleiblem6  22604  m2detleiblem3  22607  m2detleiblem4  22608  m2detleib  22609  indiscld  23069  xpstopnlem1  23787  xpstopnlem2  23789  ehl2eudis  25402  i1f1lem  25669  i1f1  25670  aannenlem2  26309  taylthlem2  26354  taylthlem2OLD  26355  ppiublem2  27183  lgsdir2lem3  27307  ltsres  27643  noextendgt  27651  nolesgn2ores  27653  nosepnelem  27660  nosepdmlem  27664  nolt02o  27676  nosupno  27684  nosupbnd1lem3  27691  nosupbnd1  27695  nosupbnd2lem1  27696  noetainflem1  27718  ecgrtg  29069  elntg  29070  usgr2trlncl  29846  usgrwwlks2on  30044  umgrwwlks2on  30045  wlk2v2e  30245  eulerpathpr  30328  ex-br  30519  ex-eprel  30521  s2rnOLD  33022  trsp2cyc  33202  cyc3fv2  33217  esplyfvaln  33736  constrconj  33908  nn0constr  33924  subfacp1lem3  35383  kur14lem7  35413  ex-sategoelel12  35628  onpsstopbas  36631  onint1  36650  bj-inftyexpidisj  37543  kelac2  43514  omnord1ex  43753  oege2  43756  oenord1ex  43764  oenord1  43765  oaomoencom  43766  oenassex  43767  omcl3g  43783  onnoxp  43881  fvrcllb1d  44143  relexp1idm  44162  corcltrcl  44187  cotrclrcl  44190  clsk1indlem1  44493  mnuprdlem2  44721  mnuprdlem3  44722  mnurndlem1  44729  refsum2cnlem1  45489  limsup10exlem  46221  fourierdlem103  46658  fourierdlem104  46659  ioorrnopn  46754  ioorrnopnxr  46756  stgr1  48452  grlimgrtrilem1  48492  gpgiedgdmellem  48537  gpgvtx1  48545  gpg3kgrtriex  48580  pglem  48582  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem9  48594  grlimedgnedg  48622  zlmodzxzscm  48848  zlmodzxzldeplem3  48993  nn0sumshdiglemB  49111  2arympt  49140  rrx2pyel  49203  rrx2linesl  49234  2sphere0  49241  termc2  50008