Theorem prid2 4665

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

Syntax hints:   ∈ wcel 2112  Vcvv 3398  {cpr 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-sn 4528  df-pr 4530

This theorem is referenced by:  opi2  5338  opeluu  5339  opthwiener  5382  dmrnssfld  5824  funopg  6392  fprb  6987  2dom  8685  djuss  9501  dfac2b  9709  brdom7disj  10110  brdom6disj  10111  cnelprrecn  10787  mnfxr  10855  seqexw  13555  m1expcl2  13622  hash2prb  14003  pr2pwpr  14010  sadcf  15975  fnpr2ob  17017  setcepi  17548  setc2obas  17554  setc2ohom  17555  cat1  17557  grpss  18339  efgi1  19065  frgpuptinv  19115  dmdprdpr  19390  dprdpr  19391  cnmsgnsubg  20493  m2detleiblem6  21477  m2detleiblem3  21480  m2detleiblem4  21481  m2detleib  21482  indiscld  21942  xpstopnlem1  22660  xpstopnlem2  22662  ehl2eudis  24273  i1f1lem  24540  i1f1  24541  aannenlem2  25176  taylthlem2  25220  ppiublem2  26038  lgsdir2lem3  26162  ecgrtg  27028  elntg  27029  usgr2trlncl  27801  umgrwwlks2on  27995  wlk2v2e  28194  eulerpathpr  28277  ex-br  28468  ex-eprel  28470  s2rn  30892  trsp2cyc  31063  cyc3fv2  31078  subfacp1lem3  32811  kur14lem7  32841  ex-sategoelel12  33056  sltres  33551  noextendgt  33559  nolesgn2ores  33561  nosepnelem  33568  nosepdmlem  33572  nolt02o  33584  nosupno  33592  nosupbnd1lem3  33599  nosupbnd1  33603  nosupbnd2lem1  33604  noetainflem1  33626  onpsstopbas  34305  onint1  34324  bj-inftyexpidisj  35065  kelac2  40534  fvrcllb1d  40921  relexp1idm  40940  corcltrcl  40965  cotrclrcl  40968  clsk1indlem1  41273  mnuprdlem2  41505  mnuprdlem3  41506  mnurndlem1  41513  refsum2cnlem1  42194  limsup10exlem  42931  fourierdlem103  43368  fourierdlem104  43369  ioorrnopn  43464  ioorrnopnxr  43466  zlmodzxzscm  45309  zlmodzxzldeplem3  45459  nn0sumshdiglemB  45582  2arympt  45611  rrx2pyel  45674  rrx2linesl  45705  2sphere0  45712