Theorem prid2 4723

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  {cpr 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4584  df-pr 4586

This theorem is referenced by:  opi2  5438  opeluu  5439  opthwiener  5484  dmrnssfld  5951  funopg  6556  fprb  7179  1oelpr  8449  nlim2  8460  2dom  9012  djuss  9879  dfac2b  10088  brdom7disj  10489  brdom6disj  10490  cnelprrecn  11167  1elpr01  11178  mnfxr  11240  seqexw  14031  m1expcl2  14099  hash2prb  14486  pr2pwpr  14493  sadcf  16488  fnpr2ob  17589  setcepi  18122  setc2obas  18128  setc2ohom  18129  cat1  18131  grpss  18997  efgi1  19762  frgpuptinv  19812  dmdprdpr  20092  dprdpr  20093  cnmsgnsubg  21630  m2detleiblem6  22687  m2detleiblem3  22690  m2detleiblem4  22691  m2detleib  22692  indiscld  23152  xpstopnlem1  23870  xpstopnlem2  23872  ehl2eudis  25485  i1f1lem  25752  i1f1  25753  aannenlem2  26394  taylthlem2  26438  ppiublem2  27268  lgsdir2lem3  27392  ltsres  27727  noextendgt  27735  nolesgn2ores  27737  nosepnelem  27744  nosepdmlem  27748  nolt02o  27760  nosupno  27768  nosupbnd1lem3  27775  nosupbnd1  27779  nosupbnd2lem1  27780  noetainflem1  27802  ecgrtg  29185  elntg  29186  usgr2trlncl  29961  usgrwwlks2on  30159  umgrwwlks2on  30160  wlk2v2e  30360  eulerpathpr  30443  ex-br  30634  ex-eprel  30636  s2rnOLD  33123  trsp2cyc  33304  cyc3fv2  33319  esplyfvaln  33872  nn0constr  34059  subfacp1lem3  35533  kur14lem7  35563  ex-sategoelel12  35778  onpsstopbas  36791  onint1  36810  bj-inftyexpidisj  37703  kelac2  43643  omnord1ex  43882  oege2  43885  oenord1ex  43893  oenord1  43894  oenassex  43896  omcl3g  43912  onnoxp  44010  fvrcllb1d  44272  relexp1idm  44291  corcltrcl  44316  cotrclrcl  44319  clsk1indlem1  44622  mnuprdlem2  44850  mnuprdlem3  44851  mnurndlem1  44858  refsum2cnlem1  45618  limsup10exlem  46347  fourierdlem103  46784  fourierdlem104  46785  ioorrnopn  46880  ioorrnopnxr  46882  stgr1  48584  grlimgrtrilem1  48624  gpgiedgdmellem  48669  gpgvtx1  48677  gpg3kgrtriex  48712  pglem  48714  gpgprismgr4cycllem3  48720  gpgprismgr4cycllem9  48726  zlmodzxzscm  48980  zlmodzxzldeplem3  49125  nn0sumshdiglemB  49243  2arympt  49272  rrx2pyel  49335  rrx2linesl  49366  2sphere0  49373  termc2  50140