Theorem prid2 4729

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592

This theorem is referenced by:  opi2  5451  opeluu  5452  opthwiener  5497  dmrnssfld  5964  funopg  6570  fprb  7192  1oelpr  8460  2dom  9023  dfac2b  10110  brdom7disj  10510  brdom6disj  10511  cnelprrecn  11188  1elpr01  11199  mnfxr  11261  seqexw  14049  m1expcl2  14117  hash2prb  14505  pr2pwpr  14512  cat1  18149  grpss  19016  dmdprdpr  20116  cnmsgnsubg  21727  m2detleiblem6  22783  m2detleiblem3  22786  m2detleiblem4  22787  m2detleib  22788  indiscld  23248  ehl2eudis  25581  aannenlem2  26492  taylthlem2  26537  ppiublem2  27367  lgsdir2lem3  27491  ltsres  27826  noextendgt  27834  nolesgn2ores  27836  nosepnelem  27843  nosepdmlem  27847  nolt02o  27859  nosupno  27867  nosupbnd1lem3  27874  nosupbnd1  27878  nosupbnd2lem1  27879  noetainflem1  27901  ecgrtg  29333  elntg  29334  wlk2v2e  30508  eulerpathpr  30591  ex-br  30782  ex-eprel  30784  s2rnOLD  33264  trsp2cyc  33443  subfacp1lem3  35674  kur14lem7  35704  ex-sategoelel12  35919  onpsstopbas  36961  onint1  36980  bj-inftyexpidisj  37874  kelac2  43812  onnoxp  44179  clsk1indlem1  44791  mnuprdlem2  45003  mnuprdlem3  45004  mnurndlem1  45011  refsum2cnlem1  45777  fourierdlem103  46943  fourierdlem104  46944  ioorrnopn  47039  ioorrnopnxr  47041  grlimgrtrilem1  48786  pglem  48876  zlmodzxzldeplem3  49302  nn0sumshdiglemB  49420  rrx2pyel  49512  rrx2linesl  49543  2sphere0  49550  termc2  50316