Theorem elpri 4580

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

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2108  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  nelpri  4587  nelprd  4589  tppreqb  4735  elpreqpr  4794  elpr2elpr  4796  prproe  4834  3elpr2eq  4835  opth1  5384  0nelop  5404  ftpg  7010  2oconcl  8295  cantnflem2  9378  eldju1st  9612  m1expcl2  13732  hash2pwpr  14118  bitsinv1lem  16076  prm23lt5  16443  fnpr2ob  17186  fvprif  17189  xpsfeq  17191  pmtrprfval  19010  m1expaddsub  19021  psgnprfval  19044  frgpuptinv  19292  frgpup3lem  19298  simpgnsgeqd  19619  2nsgsimpgd  19620  simpgnsgbid  19621  cnmsgnsubg  20694  zrhpsgnelbas  20711  mdetralt  21665  m2detleiblem1  21681  indiscld  22150  cnindis  22351  connclo  22474  txindis  22693  xpsxmetlem  23440  xpsmet  23443  ishl2  24439  recnprss  24973  recnperf  24974  dvlip2  25064  coseq0negpitopi  25565  pythag  25872  reasinsin  25951  scvxcvx  26040  perfectlem2  26283  lgslem4  26353  lgseisenlem2  26429  2lgsoddprmlem3  26467  usgredg4  27487  konigsberg  28522  ex-pr  28695  elpreq  30779  1neg1t1neg1  30974  tocyc01  31287  signswch  32440  kur14lem7  33074  poimirlem31  35735  ftc1anclem2  35778  wepwsolem  40783  relexp01min  41210  clsk1indlem1  41544  mnuprdlem1  41779  mnuprdlem2  41780  mnuprdlem3  41781  mnurndlem1  41788  ssrecnpr  41815  seff  41816  sblpnf  41817  expgrowthi  41840  dvconstbi  41841  sumpair  42467  refsum2cnlem1  42469  iooinlbub  42929  elprn1  43064  elprn2  43065  cncfiooicclem1  43324  dvmptconst  43346  dvmptidg  43348  dvmulcncf  43356  dvdivcncf  43358  elprneb  44410  perfectALTVlem2  45062  0dig2pr01  45844  prelrrx2b  45948  setc2othin  46225