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 2842	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2108  Vcvv 3488  {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 2110  ax-9 2118  ax-ext 2711

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 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  opi2  5489  opeluu  5490  opthwiener  5533  dmrnssfld  5996  funopg  6612  fprb  7231  nlim2  8546  2dom  9095  djuss  9989  dfac2b  10200  brdom7disj  10600  brdom6disj  10601  cnelprrecn  11277  mnfxr  11347  seqexw  14068  m1expcl2  14136  hash2prb  14521  pr2pwpr  14528  sadcf  16499  fnpr2ob  17618  setcepi  18155  setc2obas  18161  setc2ohom  18162  cat1  18164  grpss  18994  efgi1  19763  frgpuptinv  19813  dmdprdpr  20093  dprdpr  20094  cnmsgnsubg  21618  m2detleiblem6  22653  m2detleiblem3  22656  m2detleiblem4  22657  m2detleib  22658  indiscld  23120  xpstopnlem1  23838  xpstopnlem2  23840  ehl2eudis  25475  i1f1lem  25743  i1f1  25744  aannenlem2  26389  taylthlem2  26434  taylthlem2OLD  26435  ppiublem2  27265  lgsdir2lem3  27389  sltres  27725  noextendgt  27733  nolesgn2ores  27735  nosepnelem  27742  nosepdmlem  27746  nolt02o  27758  nosupno  27766  nosupbnd1lem3  27773  nosupbnd1  27777  nosupbnd2lem1  27778  noetainflem1  27800  ecgrtg  29016  elntg  29017  usgr2trlncl  29796  umgrwwlks2on  29990  wlk2v2e  30189  eulerpathpr  30272  ex-br  30463  ex-eprel  30465  s2rnOLD  32910  trsp2cyc  33116  cyc3fv2  33131  constrconj  33735  subfacp1lem3  35150  kur14lem7  35180  ex-sategoelel12  35395  onpsstopbas  36396  onint1  36415  bj-inftyexpidisj  37176  kelac2  43022  omnord1ex  43266  oege2  43269  oenord1ex  43277  oenord1  43278  oaomoencom  43279  oenassex  43280  omcl3g  43296  onno  43395  fvrcllb1d  43657  relexp1idm  43676  corcltrcl  43701  cotrclrcl  43704  clsk1indlem1  44007  mnuprdlem2  44242  mnuprdlem3  44243  mnurndlem1  44250  refsum2cnlem1  44937  limsup10exlem  45693  fourierdlem103  46130  fourierdlem104  46131  ioorrnopn  46226  ioorrnopnxr  46228  grlimgrtrilem1  47818  zlmodzxzscm  48082  zlmodzxzldeplem3  48231  nn0sumshdiglemB  48354  2arympt  48383  rrx2pyel  48446  rrx2linesl  48477  2sphere0  48484