Theorem prid2 4720

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  opi2  5417  opeluu  5418  opthwiener  5462  dmrnssfld  5923  funopg  6526  fprb  7140  nlim2  8417  2dom  8969  djuss  9834  dfac2b  10043  brdom7disj  10443  brdom6disj  10444  cnelprrecn  11121  mnfxr  11191  seqexw  13942  m1expcl2  14010  hash2prb  14397  pr2pwpr  14404  sadcf  16382  fnpr2ob  17481  setcepi  18014  setc2obas  18020  setc2ohom  18021  cat1  18023  grpss  18886  efgi1  19652  frgpuptinv  19702  dmdprdpr  19982  dprdpr  19983  cnmsgnsubg  21534  m2detleiblem6  22572  m2detleiblem3  22575  m2detleiblem4  22576  m2detleib  22577  indiscld  23037  xpstopnlem1  23755  xpstopnlem2  23757  ehl2eudis  25380  i1f1lem  25648  i1f1  25649  aannenlem2  26295  taylthlem2  26340  taylthlem2OLD  26341  ppiublem2  27172  lgsdir2lem3  27296  ltsres  27632  noextendgt  27640  nolesgn2ores  27642  nosepnelem  27649  nosepdmlem  27653  nolt02o  27665  nosupno  27673  nosupbnd1lem3  27680  nosupbnd1  27684  nosupbnd2lem1  27685  noetainflem1  27707  ecgrtg  29058  elntg  29059  usgr2trlncl  29835  usgrwwlks2on  30033  umgrwwlks2on  30034  wlk2v2e  30234  eulerpathpr  30317  ex-br  30508  ex-eprel  30510  s2rnOLD  33028  trsp2cyc  33207  cyc3fv2  33222  constrconj  33904  nn0constr  33920  subfacp1lem3  35378  kur14lem7  35408  ex-sategoelel12  35623  onpsstopbas  36626  onint1  36645  bj-inftyexpidisj  37417  kelac2  43328  omnord1ex  43567  oege2  43570  oenord1ex  43578  oenord1  43579  oaomoencom  43580  oenassex  43581  omcl3g  43597  onnoxp  43695  fvrcllb1d  43957  relexp1idm  43976  corcltrcl  44001  cotrclrcl  44004  clsk1indlem1  44307  mnuprdlem2  44535  mnuprdlem3  44536  mnurndlem1  44543  refsum2cnlem1  45303  limsup10exlem  46037  fourierdlem103  46474  fourierdlem104  46475  ioorrnopn  46570  ioorrnopnxr  46572  stgr1  48228  grlimgrtrilem1  48268  gpgiedgdmellem  48313  gpgvtx1  48321  gpg3kgrtriex  48356  pglem  48358  gpgprismgr4cycllem3  48364  gpgprismgr4cycllem9  48370  grlimedgnedg  48398  zlmodzxzscm  48624  zlmodzxzldeplem3  48769  nn0sumshdiglemB  48887  2arympt  48916  rrx2pyel  48979  rrx2linesl  49010  2sphere0  49017  termc2  49784