Theorem elpri 4584

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

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1539   ∈ wcel 2107  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-sn 4563  df-pr 4565

This theorem is referenced by:  nelpri  4591  nelprd  4593  tppreqb  4739  elpreqpr  4798  elpr2elpr  4800  prproe  4838  3elpr2eq  4839  opth1  5391  0nelop  5411  ftpg  7037  2oconcl  8342  cantnflem2  9457  eldju1st  9690  m1expcl2  13813  hash2pwpr  14199  bitsinv1lem  16157  prm23lt5  16524  fnpr2ob  17278  fvprif  17281  xpsfeq  17283  pmtrprfval  19104  m1expaddsub  19115  psgnprfval  19138  frgpuptinv  19386  frgpup3lem  19392  simpgnsgeqd  19713  2nsgsimpgd  19714  simpgnsgbid  19715  cnmsgnsubg  20791  zrhpsgnelbas  20808  mdetralt  21766  m2detleiblem1  21782  indiscld  22251  cnindis  22452  connclo  22575  txindis  22794  xpsxmetlem  23541  xpsmet  23544  ishl2  24543  recnprss  25077  recnperf  25078  dvlip2  25168  coseq0negpitopi  25669  pythag  25976  reasinsin  26055  scvxcvx  26144  perfectlem2  26387  lgslem4  26457  lgseisenlem2  26533  2lgsoddprmlem3  26571  usgredg4  27593  konigsberg  28630  ex-pr  28803  elpreq  30887  1neg1t1neg1  31081  tocyc01  31394  signswch  32549  kur14lem7  33183  poimirlem31  35817  ftc1anclem2  35860  wepwsolem  40874  relexp01min  41328  clsk1indlem1  41662  mnuprdlem1  41897  mnuprdlem2  41898  mnuprdlem3  41899  mnurndlem1  41906  ssrecnpr  41933  seff  41934  sblpnf  41935  expgrowthi  41958  dvconstbi  41959  sumpair  42585  refsum2cnlem1  42587  iooinlbub  43046  elprn1  43181  elprn2  43182  cncfiooicclem1  43441  dvmptconst  43463  dvmptidg  43465  dvmulcncf  43473  dvdivcncf  43475  elprneb  44534  perfectALTVlem2  45185  0dig2pr01  45967  prelrrx2b  46071  setc2othin  46348