Theorem elpri 4604

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  elprn1  4608  elprn2  4609  nelpri  4612  nelprd  4614  tppreqb  4764  elpreqpr  4821  elpr2elpr  4823  prproe  4832  3elpr2eq  4833  opth1  5443  0nelop  5467  ftpg  7161  fvf1pr  7316  2oconcl  8515  cantnflem2  9695  eldju1st  10008  m1expcl2  14232  hash2pwpr  14625  bitsinv1lem  16617  prm23lt5  16998  fnpr2ob  17736  fvprif  17739  xpsfeq  17741  ex-chn2  18818  pmtrprfval  19707  m1expaddsub  19718  psgnprfval  19741  frgpuptinv  19991  frgpup3lem  19997  simpgnsgeqd  20323  2nsgsimpgd  20324  simpgnsgbid  20325  drngidl  21545  cnmsgnsubg  21889  zrhpsgnelbas  21906  mdetralt  22929  m2detleiblem1  22945  indiscld  23415  cnindis  23616  connclo  23739  txindis  23959  xpsxmetlem  24704  xpsmet  24707  ishl2  25697  recnprss  26230  recnperf  26231  dvlip2  26321  coseq0negpitopi  26838  pythag  27151  reasinsin  27230  scvxcvx  27319  perfectlem2  27563  lgslem4  27633  lgseisenlem2  27709  2lgsoddprmlem3  27747  usgredg4  29804  konigsberg  30864  ex-pr  31037  elpreq  33172  1neg1t1neg1  33377  tocyc01  33726  drng0mxidl  34047  ply1dg3rt0irred  34163  rtelextdg2  34406  constrconj  34424  signswch  35237  kur14lem7  36064  poimirlem31  38663  ftc1anclem2  38706  wepwsolem  44143  omabs2  44428  omcl3g  44430  relexp01min  44807  clsk1indlem1  45139  mnuprdlem1  45350  mnuprdlem2  45351  mnuprdlem3  45352  mnurndlem1  45359  ssrecnpr  45386  seff  45387  sblpnf  45388  expgrowthi  45411  dvconstbi  45412  sumpair  46146  refsum2cnlem1  46148  iooinlbub  46607  cncfiooicclem1  46997  dvmptconst  47019  dvmptidg  47021  dvmulcncf  47029  dvdivcncf  47031  elprneb  48193  minusmodnep2tmod  48523  perfectALTVlem2  48914  grtriclwlk3  49137  gpgcubic  49271  gpg5nbgr3star  49273  gpgprismgr4cycllem3  49289  gpgprismgr4cycllem7  49293  gpgprismgr4cycllem10  49296  pgnbgreunbgr  49317  0dig2pr01  49816  infsubc  50268  infsubc2  50269  setc2othin  50695