Theorem elpri 4649

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

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1541   ∈ wcel 2106  {cpr 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-sn 4628  df-pr 4630

This theorem is referenced by:  nelpri  4656  nelprd  4658  tppreqb  4807  elpreqpr  4866  elpr2elpr  4868  prproe  4905  3elpr2eq  4906  opth1  5474  0nelop  5495  ftpg  7150  2oconcl  8499  cantnflem2  9681  eldju1st  9914  m1expcl2  14047  hash2pwpr  14433  bitsinv1lem  16378  prm23lt5  16743  fnpr2ob  17500  fvprif  17503  xpsfeq  17505  pmtrprfval  19349  m1expaddsub  19360  psgnprfval  19383  frgpuptinv  19633  frgpup3lem  19639  simpgnsgeqd  19965  2nsgsimpgd  19966  simpgnsgbid  19967  cnmsgnsubg  21121  zrhpsgnelbas  21138  mdetralt  22101  m2detleiblem1  22117  indiscld  22586  cnindis  22787  connclo  22910  txindis  23129  xpsxmetlem  23876  xpsmet  23879  ishl2  24878  recnprss  25412  recnperf  25413  dvlip2  25503  coseq0negpitopi  26004  pythag  26311  reasinsin  26390  scvxcvx  26479  perfectlem2  26722  lgslem4  26792  lgseisenlem2  26868  2lgsoddprmlem3  26906  usgredg4  28463  konigsberg  29499  ex-pr  29672  elpreq  31754  1neg1t1neg1  31949  tocyc01  32264  drngidl  32539  drng0mxidl  32580  signswch  33560  kur14lem7  34191  poimirlem31  36507  ftc1anclem2  36550  wepwsolem  41769  omabs2  42067  omcl3g  42069  relexp01min  42449  clsk1indlem1  42781  mnuprdlem1  43016  mnuprdlem2  43017  mnuprdlem3  43018  mnurndlem1  43025  ssrecnpr  43052  seff  43053  sblpnf  43054  expgrowthi  43077  dvconstbi  43078  sumpair  43704  refsum2cnlem1  43706  iooinlbub  44200  elprn1  44335  elprn2  44336  cncfiooicclem1  44595  dvmptconst  44617  dvmptidg  44619  dvmulcncf  44627  dvdivcncf  44629  elprneb  45725  perfectALTVlem2  46376  0dig2pr01  47249  prelrrx2b  47353  setc2othin  47629