Theorem elpri 4616

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109  {cpr 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  nelpri  4622  nelprd  4624  tppreqb  4772  elpreqpr  4834  elpr2elpr  4836  prproe  4872  3elpr2eq  4873  opth1  5438  0nelop  5459  ftpg  7131  fvf1pr  7285  2oconcl  8470  cantnflem2  9650  eldju1st  9883  m1expcl2  14057  hash2pwpr  14448  bitsinv1lem  16418  prm23lt5  16792  fnpr2ob  17528  fvprif  17531  xpsfeq  17533  pmtrprfval  19424  m1expaddsub  19435  psgnprfval  19458  frgpuptinv  19708  frgpup3lem  19714  simpgnsgeqd  20040  2nsgsimpgd  20041  simpgnsgbid  20042  cnmsgnsubg  21493  zrhpsgnelbas  21510  mdetralt  22502  m2detleiblem1  22518  indiscld  22985  cnindis  23186  connclo  23309  txindis  23528  xpsxmetlem  24274  xpsmet  24277  ishl2  25277  recnprss  25812  recnperf  25813  dvlip2  25907  coseq0negpitopi  26419  pythag  26734  reasinsin  26813  scvxcvx  26903  perfectlem2  27148  lgslem4  27218  lgseisenlem2  27294  2lgsoddprmlem3  27332  usgredg4  29151  konigsberg  30193  ex-pr  30366  elpreq  32464  1neg1t1neg1  32668  tocyc01  33082  drngidl  33411  drng0mxidl  33454  ply1dg3rt0irred  33558  rtelextdg2  33724  constrconj  33742  signswch  34559  kur14lem7  35206  poimirlem31  37652  ftc1anclem2  37695  wepwsolem  43038  omabs2  43328  omcl3g  43330  relexp01min  43709  clsk1indlem1  44041  mnuprdlem1  44268  mnuprdlem2  44269  mnuprdlem3  44270  mnurndlem1  44277  ssrecnpr  44304  seff  44305  sblpnf  44306  expgrowthi  44329  dvconstbi  44330  sumpair  45036  refsum2cnlem1  45038  iooinlbub  45506  elprn1  45638  elprn2  45639  cncfiooicclem1  45898  dvmptconst  45920  dvmptidg  45922  dvmulcncf  45930  dvdivcncf  45932  elprneb  47034  minusmodnep2tmod  47358  perfectALTVlem2  47727  grtriclwlk3  47948  gpgcubic  48074  gpg5nbgr3star  48076  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098  pgnbgreunbgr  48119  0dig2pr01  48603  prelrrx2b  48707  infsubc  49053  infsubc2  49054  setc2othin  49459