Theorem prid2 4696

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  opi2  5378  opeluu  5379  opthwiener  5422  dmrnssfld  5868  funopg  6452  fprb  7051  2dom  8774  djuss  9609  dfac2b  9817  brdom7disj  10218  brdom6disj  10219  cnelprrecn  10895  mnfxr  10963  seqexw  13665  m1expcl2  13732  hash2prb  14114  pr2pwpr  14121  sadcf  16088  fnpr2ob  17186  setcepi  17719  setc2obas  17725  setc2ohom  17726  cat1  17728  grpss  18512  efgi1  19242  frgpuptinv  19292  dmdprdpr  19567  dprdpr  19568  cnmsgnsubg  20694  m2detleiblem6  21683  m2detleiblem3  21686  m2detleiblem4  21687  m2detleib  21688  indiscld  22150  xpstopnlem1  22868  xpstopnlem2  22870  ehl2eudis  24491  i1f1lem  24758  i1f1  24759  aannenlem2  25394  taylthlem2  25438  ppiublem2  26256  lgsdir2lem3  26380  ecgrtg  27254  elntg  27255  usgr2trlncl  28029  umgrwwlks2on  28223  wlk2v2e  28422  eulerpathpr  28505  ex-br  28696  ex-eprel  28698  s2rn  31120  trsp2cyc  31292  cyc3fv2  31307  subfacp1lem3  33044  kur14lem7  33074  ex-sategoelel12  33289  sltres  33792  noextendgt  33800  nolesgn2ores  33802  nosepnelem  33809  nosepdmlem  33813  nolt02o  33825  nosupno  33833  nosupbnd1lem3  33840  nosupbnd1  33844  nosupbnd2lem1  33845  noetainflem1  33867  onpsstopbas  34546  onint1  34565  bj-inftyexpidisj  35308  kelac2  40806  fvrcllb1d  41192  relexp1idm  41211  corcltrcl  41236  cotrclrcl  41239  clsk1indlem1  41544  mnuprdlem2  41780  mnuprdlem3  41781  mnurndlem1  41788  refsum2cnlem1  42469  limsup10exlem  43203  fourierdlem103  43640  fourierdlem104  43641  ioorrnopn  43736  ioorrnopnxr  43738  zlmodzxzscm  45581  zlmodzxzldeplem3  45731  nn0sumshdiglemB  45854  2arympt  45883  rrx2pyel  45946  rrx2linesl  45977  2sphere0  45984