Theorem elpri 4643

Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.)

Assertion

Ref	Expression
elpri	⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Proof of Theorem elpri

Step	Hyp	Ref	Expression
1		elprg 4642	. 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
2	1	ibi 267	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1533   ∈ wcel 2098  {cpr 4623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-un 3946  df-sn 4622  df-pr 4624

This theorem is referenced by:  nelpri  4650  nelprd  4652  tppreqb  4801  elpreqpr  4860  elpr2elpr  4862  prproe  4898  3elpr2eq  4899  opth1  5466  0nelop  5487  ftpg  7147  2oconcl  8499  cantnflem2  9682  eldju1st  9915  m1expcl2  14049  hash2pwpr  14435  bitsinv1lem  16381  prm23lt5  16748  fnpr2ob  17505  fvprif  17508  xpsfeq  17510  pmtrprfval  19399  m1expaddsub  19410  psgnprfval  19433  frgpuptinv  19683  frgpup3lem  19689  simpgnsgeqd  20015  2nsgsimpgd  20016  simpgnsgbid  20017  cnmsgnsubg  21440  zrhpsgnelbas  21457  mdetralt  22434  m2detleiblem1  22450  indiscld  22919  cnindis  23120  connclo  23243  txindis  23462  xpsxmetlem  24209  xpsmet  24212  ishl2  25222  recnprss  25757  recnperf  25758  dvlip2  25852  coseq0negpitopi  26357  pythag  26668  reasinsin  26747  scvxcvx  26837  perfectlem2  27082  lgslem4  27152  lgseisenlem2  27228  2lgsoddprmlem3  27266  usgredg4  28946  konigsberg  29982  ex-pr  30155  elpreq  32239  1neg1t1neg1  32434  tocyc01  32748  drngidl  33023  drng0mxidl  33064  signswch  34064  kur14lem7  34694  poimirlem31  37013  ftc1anclem2  37056  wepwsolem  42298  omabs2  42596  omcl3g  42598  relexp01min  42978  clsk1indlem1  43310  mnuprdlem1  43545  mnuprdlem2  43546  mnuprdlem3  43547  mnurndlem1  43554  ssrecnpr  43581  seff  43582  sblpnf  43583  expgrowthi  43606  dvconstbi  43607  sumpair  44233  refsum2cnlem1  44235  iooinlbub  44724  elprn1  44859  elprn2  44860  cncfiooicclem1  45119  dvmptconst  45141  dvmptidg  45143  dvmulcncf  45151  dvdivcncf  45153  elprneb  46249  perfectALTVlem2  46900  0dig2pr01  47509  prelrrx2b  47613  setc2othin  47888