Theorem elpri 4586

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 4585	. 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
2	1	ibi 268	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  elprn1  4590  elprn2  4591  nelpri  4594  nelprd  4596  tppreqb  4745  elpreqpr  4805  elpr2elpr  4807  prproe  4843  3elpr2eq  4844  opth1  5422  0nelop  5444  ftpg  7106  fvf1pr  7258  2oconcl  8435  cantnflem2  9609  eldju1st  9845  m1expcl2  14045  hash2pwpr  14436  bitsinv1lem  16408  prm23lt5  16783  fnpr2ob  17520  fvprif  17523  xpsfeq  17525  ex-chn2  18602  pmtrprfval  19460  m1expaddsub  19471  psgnprfval  19494  frgpuptinv  19744  frgpup3lem  19750  simpgnsgeqd  20076  2nsgsimpgd  20077  simpgnsgbid  20078  cnmsgnsubg  21559  zrhpsgnelbas  21576  mdetralt  22598  m2detleiblem1  22614  indiscld  23081  cnindis  23282  connclo  23405  txindis  23624  xpsxmetlem  24369  xpsmet  24372  ishl2  25362  recnprss  25896  recnperf  25897  dvlip2  25987  coseq0negpitopi  26492  pythag  26806  reasinsin  26885  scvxcvx  26974  perfectlem2  27218  lgslem4  27288  lgseisenlem2  27364  2lgsoddprmlem3  27402  usgredg4  29311  konigsberg  30352  ex-pr  30525  elpreq  32623  1neg1t1neg1  32837  tocyc01  33206  drngidl  33523  drng0mxidl  33566  ply1dg3rt0irred  33674  rtelextdg2  33918  constrconj  33936  signswch  34752  kur14lem7  35447  poimirlem31  38025  ftc1anclem2  38068  wepwsolem  43494  omabs2  43784  omcl3g  43786  relexp01min  44164  clsk1indlem1  44496  mnuprdlem1  44723  mnuprdlem2  44724  mnuprdlem3  44725  mnurndlem1  44732  ssrecnpr  44759  seff  44760  sblpnf  44761  expgrowthi  44784  dvconstbi  44785  sumpair  45490  refsum2cnlem1  45492  iooinlbub  45953  cncfiooicclem1  46343  dvmptconst  46365  dvmptidg  46367  dvmulcncf  46375  dvdivcncf  46377  elprneb  47499  minusmodnep2tmod  47829  perfectALTVlem2  48220  grtriclwlk3  48443  gpgcubic  48577  gpg5nbgr3star  48579  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem7  48599  gpgprismgr4cycllem10  48602  pgnbgreunbgr  48623  0dig2pr01  49108  prelrrx2b  49212  infsubc  49557  infsubc2  49558  setc2othin  49963