Theorem prid2 4699

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  opi2  5384  opeluu  5385  opthwiener  5428  dmrnssfld  5879  funopg  6468  fprb  7069  nlim2  8320  2dom  8820  djuss  9678  dfac2b  9886  brdom7disj  10287  brdom6disj  10288  cnelprrecn  10964  mnfxr  11032  seqexw  13737  m1expcl2  13804  hash2prb  14186  pr2pwpr  14193  sadcf  16160  fnpr2ob  17269  setcepi  17803  setc2obas  17809  setc2ohom  17810  cat1  17812  grpss  18597  efgi1  19327  frgpuptinv  19377  dmdprdpr  19652  dprdpr  19653  cnmsgnsubg  20782  m2detleiblem6  21775  m2detleiblem3  21778  m2detleiblem4  21779  m2detleib  21780  indiscld  22242  xpstopnlem1  22960  xpstopnlem2  22962  ehl2eudis  24586  i1f1lem  24853  i1f1  24854  aannenlem2  25489  taylthlem2  25533  ppiublem2  26351  lgsdir2lem3  26475  ecgrtg  27351  elntg  27352  usgr2trlncl  28128  umgrwwlks2on  28322  wlk2v2e  28521  eulerpathpr  28604  ex-br  28795  ex-eprel  28797  s2rn  31218  trsp2cyc  31390  cyc3fv2  31405  subfacp1lem3  33144  kur14lem7  33174  ex-sategoelel12  33389  sltres  33865  noextendgt  33873  nolesgn2ores  33875  nosepnelem  33882  nosepdmlem  33886  nolt02o  33898  nosupno  33906  nosupbnd1lem3  33913  nosupbnd1  33917  nosupbnd2lem1  33918  noetainflem1  33940  onpsstopbas  34619  onint1  34638  bj-inftyexpidisj  35381  kelac2  40890  fvrcllb1d  41303  relexp1idm  41322  corcltrcl  41347  cotrclrcl  41350  clsk1indlem1  41655  mnuprdlem2  41891  mnuprdlem3  41892  mnurndlem1  41899  refsum2cnlem1  42580  limsup10exlem  43313  fourierdlem103  43750  fourierdlem104  43751  ioorrnopn  43846  ioorrnopnxr  43848  zlmodzxzscm  45693  zlmodzxzldeplem3  45843  nn0sumshdiglemB  45966  2arympt  45995  rrx2pyel  46058  rrx2linesl  46089  2sphere0  46096