Theorem elpri 4651

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1542   ∈ wcel 2107  {cpr 4631

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  nelpri  4658  nelprd  4660  tppreqb  4809  elpreqpr  4868  elpr2elpr  4870  prproe  4907  3elpr2eq  4908  opth1  5476  0nelop  5497  ftpg  7154  2oconcl  8503  cantnflem2  9685  eldju1st  9918  m1expcl2  14051  hash2pwpr  14437  bitsinv1lem  16382  prm23lt5  16747  fnpr2ob  17504  fvprif  17507  xpsfeq  17509  pmtrprfval  19355  m1expaddsub  19366  psgnprfval  19389  frgpuptinv  19639  frgpup3lem  19645  simpgnsgeqd  19971  2nsgsimpgd  19972  simpgnsgbid  19973  cnmsgnsubg  21130  zrhpsgnelbas  21147  mdetralt  22110  m2detleiblem1  22126  indiscld  22595  cnindis  22796  connclo  22919  txindis  23138  xpsxmetlem  23885  xpsmet  23888  ishl2  24887  recnprss  25421  recnperf  25422  dvlip2  25512  coseq0negpitopi  26013  pythag  26322  reasinsin  26401  scvxcvx  26490  perfectlem2  26733  lgslem4  26803  lgseisenlem2  26879  2lgsoddprmlem3  26917  usgredg4  28474  konigsberg  29510  ex-pr  29683  elpreq  31767  1neg1t1neg1  31962  tocyc01  32277  drngidl  32551  drng0mxidl  32592  signswch  33572  kur14lem7  34203  poimirlem31  36519  ftc1anclem2  36562  wepwsolem  41784  omabs2  42082  omcl3g  42084  relexp01min  42464  clsk1indlem1  42796  mnuprdlem1  43031  mnuprdlem2  43032  mnuprdlem3  43033  mnurndlem1  43040  ssrecnpr  43067  seff  43068  sblpnf  43069  expgrowthi  43092  dvconstbi  43093  sumpair  43719  refsum2cnlem1  43721  iooinlbub  44214  elprn1  44349  elprn2  44350  cncfiooicclem1  44609  dvmptconst  44631  dvmptidg  44633  dvmulcncf  44641  dvdivcncf  44643  elprneb  45739  perfectALTVlem2  46390  0dig2pr01  47296  prelrrx2b  47400  setc2othin  47676