Theorem prid2 4788

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

Syntax hints:   ∈ wcel 2103  Vcvv 3482  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3484  df-un 3975  df-sn 4649  df-pr 4651

This theorem is referenced by:  opi2  5492  opeluu  5493  opthwiener  5537  dmrnssfld  5995  funopg  6611  fprb  7229  nlim2  8542  2dom  9091  djuss  9985  dfac2b  10196  brdom7disj  10596  brdom6disj  10597  cnelprrecn  11273  mnfxr  11343  seqexw  14064  m1expcl2  14132  hash2prb  14517  pr2pwpr  14524  sadcf  16493  fnpr2ob  17613  setcepi  18150  setc2obas  18156  setc2ohom  18157  cat1  18159  grpss  18989  efgi1  19758  frgpuptinv  19808  dmdprdpr  20088  dprdpr  20089  cnmsgnsubg  21613  m2detleiblem6  22646  m2detleiblem3  22649  m2detleiblem4  22650  m2detleib  22651  indiscld  23113  xpstopnlem1  23831  xpstopnlem2  23833  ehl2eudis  25468  i1f1lem  25736  i1f1  25737  aannenlem2  26381  taylthlem2  26426  taylthlem2OLD  26427  ppiublem2  27256  lgsdir2lem3  27380  sltres  27716  noextendgt  27724  nolesgn2ores  27726  nosepnelem  27733  nosepdmlem  27737  nolt02o  27749  nosupno  27757  nosupbnd1lem3  27764  nosupbnd1  27768  nosupbnd2lem1  27769  noetainflem1  27791  ecgrtg  29007  elntg  29008  usgr2trlncl  29787  umgrwwlks2on  29981  wlk2v2e  30180  eulerpathpr  30263  ex-br  30454  ex-eprel  30456  s2rnOLD  32902  trsp2cyc  33108  cyc3fv2  33123  constrconj  33727  subfacp1lem3  35142  kur14lem7  35172  ex-sategoelel12  35387  onpsstopbas  36343  onint1  36362  bj-inftyexpidisj  37124  kelac2  42962  omnord1ex  43206  oege2  43209  oenord1ex  43217  oenord1  43218  oaomoencom  43219  oenassex  43220  omcl3g  43236  onno  43335  fvrcllb1d  43597  relexp1idm  43616  corcltrcl  43641  cotrclrcl  43644  clsk1indlem1  43947  mnuprdlem2  44182  mnuprdlem3  44183  mnurndlem1  44190  refsum2cnlem1  44871  limsup10exlem  45627  fourierdlem103  46064  fourierdlem104  46065  ioorrnopn  46160  ioorrnopnxr  46162  zlmodzxzscm  48000  zlmodzxzldeplem3  48149  nn0sumshdiglemB  48272  2arympt  48301  rrx2pyel  48364  rrx2linesl  48395  2sphere0  48402