Theorem prid2 4734

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  opi2  5452  opeluu  5453  opthwiener  5498  dmrnssfld  5965  funopg  6571  fprb  7193  1oelpr  8464  nlim2  8475  2dom  9027  djuss  9906  dfac2b  10114  brdom7disj  10515  brdom6disj  10516  cnelprrecn  11193  1elpr01  11204  mnfxr  11266  seqexw  14053  m1expcl2  14121  hash2prb  14509  pr2pwpr  14516  sadcf  16511  fnpr2ob  17612  setcepi  18145  setc2obas  18151  setc2ohom  18152  cat1  18154  grpss  19021  efgi1  19791  frgpuptinv  19841  dmdprdpr  20121  dprdpr  20122  cnmsgnsubg  21696  m2detleiblem6  22752  m2detleiblem3  22755  m2detleiblem4  22756  m2detleib  22757  indiscld  23217  xpstopnlem1  23935  xpstopnlem2  23937  ehl2eudis  25550  i1f1lem  25817  i1f1  25818  aannenlem2  26459  taylthlem2  26503  ppiublem2  27333  lgsdir2lem3  27457  ltsres  27792  noextendgt  27800  nolesgn2ores  27802  nosepnelem  27809  nosepdmlem  27813  nolt02o  27825  nosupno  27833  nosupbnd1lem3  27840  nosupbnd1  27844  nosupbnd2lem1  27845  noetainflem1  27867  ecgrtg  29274  elntg  29275  usgr2trlncl  30050  usgrwwlks2on  30248  umgrwwlks2on  30249  wlk2v2e  30449  eulerpathpr  30532  ex-br  30723  ex-eprel  30725  s2rnOLD  33205  trsp2cyc  33384  cyc3fv2  33399  esplyfvaln  33909  nn0constr  34096  subfacp1lem3  35607  kur14lem7  35637  ex-sategoelel12  35852  onpsstopbas  36864  onint1  36883  bj-inftyexpidisj  37776  kelac2  43718  omnord1ex  43957  oege2  43960  oenord1ex  43968  oenord1  43969  oenassex  43971  omcl3g  43987  onnoxp  44085  fvrcllb1d  44347  relexp1idm  44366  corcltrcl  44391  cotrclrcl  44394  clsk1indlem1  44697  mnuprdlem2  44909  mnuprdlem3  44910  mnurndlem1  44917  refsum2cnlem1  45683  limsup10exlem  46412  fourierdlem103  46849  fourierdlem104  46850  ioorrnopn  46945  ioorrnopnxr  46947  stgr1  48649  grlimgrtrilem1  48689  gpgiedgdmellem  48734  gpgvtx1  48742  gpg3kgrtriex  48777  pglem  48779  gpgprismgr4cycllem3  48785  gpgprismgr4cycllem9  48791  zlmodzxzscm  49056  zlmodzxzldeplem3  49201  nn0sumshdiglemB  49319  2arympt  49348  rrx2pyel  49411  rrx2linesl  49442  2sphere0  49449  termc2  50215