Theorem elpri 4614

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

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1570   ∈ wcel 2143  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  elprn1  4618  elprn2  4619  nelpri  4622  nelprd  4624  tppreqb  4774  elpreqpr  4833  elpr2elpr  4835  prproe  4871  3elpr2eq  4872  opth1  5459  0nelop  5481  ftpg  7155  fvf1pr  7307  2oconcl  8489  cantnflem2  9660  eldju1st  9910  m1expcl2  14123  hash2pwpr  14515  bitsinv1lem  16500  prm23lt5  16875  fnpr2ob  17613  fvprif  17616  xpsfeq  17618  ex-chn2  18695  pmtrprfval  19558  m1expaddsub  19569  psgnprfval  19592  frgpuptinv  19842  frgpup3lem  19848  simpgnsgeqd  20174  2nsgsimpgd  20175  simpgnsgbid  20176  drngidl  21366  cnmsgnsubg  21708  zrhpsgnelbas  21725  mdetralt  22746  m2detleiblem1  22762  indiscld  23229  cnindis  23430  connclo  23553  txindis  23772  xpsxmetlem  24517  xpsmet  24520  ishl2  25510  recnprss  26044  recnperf  26045  dvlip2  26135  coseq0negpitopi  26649  pythag  26963  reasinsin  27042  scvxcvx  27131  perfectlem2  27375  lgslem4  27445  lgseisenlem2  27521  2lgsoddprmlem3  27559  usgredg4  29548  konigsberg  30589  ex-pr  30762  elpreq  32855  1neg1t1neg1  33064  tocyc01  33419  drng0mxidl  33739  ply1dg3rt0irred  33855  rtelextdg2  34098  constrconj  34116  signswch  34929  kur14lem7  35685  poimirlem31  38283  ftc1anclem2  38326  wepwsolem  43752  omabs2  44042  omcl3g  44044  relexp01min  44422  clsk1indlem1  44754  mnuprdlem1  44965  mnuprdlem2  44966  mnuprdlem3  44967  mnurndlem1  44974  ssrecnpr  45001  seff  45002  sblpnf  45003  expgrowthi  45026  dvconstbi  45027  sumpair  45738  refsum2cnlem1  45740  iooinlbub  46200  cncfiooicclem1  46590  dvmptconst  46612  dvmptidg  46614  dvmulcncf  46622  dvdivcncf  46624  elprneb  47749  minusmodnep2tmod  48079  perfectALTVlem2  48470  grtriclwlk3  48693  gpgcubic  48827  gpg5nbgr3star  48829  gpgprismgr4cycllem3  48845  gpgprismgr4cycllem7  48849  gpgprismgr4cycllem10  48852  pgnbgreunbgr  48873  0dig2pr01  49373  prelrrx2b  49477  infsubc  49821  infsubc2  49822  setc2othin  50227