Theorem elpri 4608

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  elprn1  4612  elprn2  4613  nelpri  4616  nelprd  4618  tppreqb  4768  elpreqpr  4827  elpr2elpr  4829  prproe  4865  3elpr2eq  4866  opth1  5451  0nelop  5473  ftpg  7153  fvf1pr  7308  2oconcl  8490  cantnflem2  9669  eldju1st  9928  m1expcl2  14149  hash2pwpr  14541  bitsinv1lem  16531  prm23lt5  16906  fnpr2ob  17644  fvprif  17647  xpsfeq  17649  ex-chn2  18726  pmtrprfval  19614  m1expaddsub  19625  psgnprfval  19648  frgpuptinv  19898  frgpup3lem  19904  simpgnsgeqd  20230  2nsgsimpgd  20231  simpgnsgbid  20232  drngidl  21448  cnmsgnsubg  21790  zrhpsgnelbas  21807  mdetralt  22830  m2detleiblem1  22846  indiscld  23316  cnindis  23517  connclo  23640  txindis  23860  xpsxmetlem  24605  xpsmet  24608  ishl2  25598  recnprss  26131  recnperf  26132  dvlip2  26222  coseq0negpitopi  26741  pythag  27054  reasinsin  27133  scvxcvx  27222  perfectlem2  27466  lgslem4  27536  lgseisenlem2  27612  2lgsoddprmlem3  27650  usgredg4  29677  konigsberg  30737  ex-pr  30910  elpreq  33003  1neg1t1neg1  33209  tocyc01  33558  drng0mxidl  33878  ply1dg3rt0irred  33994  rtelextdg2  34237  constrconj  34255  signswch  35069  kur14lem7  35791  poimirlem31  38400  ftc1anclem2  38443  wepwsolem  43883  omabs2  44173  omcl3g  44175  relexp01min  44553  clsk1indlem1  44885  mnuprdlem1  45096  mnuprdlem2  45097  mnuprdlem3  45098  mnurndlem1  45105  ssrecnpr  45132  seff  45133  sblpnf  45134  expgrowthi  45157  dvconstbi  45158  sumpair  45869  refsum2cnlem1  45871  iooinlbub  46331  cncfiooicclem1  46721  dvmptconst  46743  dvmptidg  46745  dvmulcncf  46753  dvdivcncf  46755  elprneb  47917  minusmodnep2tmod  48247  perfectALTVlem2  48638  grtriclwlk3  48861  gpgcubic  48995  gpg5nbgr3star  48997  gpgprismgr4cycllem3  49013  gpgprismgr4cycllem7  49017  gpgprismgr4cycllem10  49020  pgnbgreunbgr  49041  0dig2pr01  49540  prelrrx2b  49644  infsubc  49986  infsubc2  49987  setc2othin  50392