Theorem elpri 4625

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  nelpri  4631  nelprd  4633  tppreqb  4781  elpreqpr  4843  elpr2elpr  4845  prproe  4881  3elpr2eq  4882  opth1  5450  0nelop  5471  ftpg  7146  fvf1pr  7300  2oconcl  8515  cantnflem2  9704  eldju1st  9937  m1expcl2  14103  hash2pwpr  14494  bitsinv1lem  16460  prm23lt5  16834  fnpr2ob  17572  fvprif  17575  xpsfeq  17577  pmtrprfval  19468  m1expaddsub  19479  psgnprfval  19502  frgpuptinv  19752  frgpup3lem  19758  simpgnsgeqd  20084  2nsgsimpgd  20085  simpgnsgbid  20086  cnmsgnsubg  21537  zrhpsgnelbas  21554  mdetralt  22546  m2detleiblem1  22562  indiscld  23029  cnindis  23230  connclo  23353  txindis  23572  xpsxmetlem  24318  xpsmet  24321  ishl2  25322  recnprss  25857  recnperf  25858  dvlip2  25952  coseq0negpitopi  26464  pythag  26779  reasinsin  26858  scvxcvx  26948  perfectlem2  27193  lgslem4  27263  lgseisenlem2  27339  2lgsoddprmlem3  27377  usgredg4  29196  konigsberg  30238  ex-pr  30411  elpreq  32509  1neg1t1neg1  32715  tocyc01  33129  drngidl  33448  drng0mxidl  33491  ply1dg3rt0irred  33595  rtelextdg2  33761  constrconj  33779  signswch  34593  kur14lem7  35234  poimirlem31  37675  ftc1anclem2  37718  wepwsolem  43066  omabs2  43356  omcl3g  43358  relexp01min  43737  clsk1indlem1  44069  mnuprdlem1  44296  mnuprdlem2  44297  mnuprdlem3  44298  mnurndlem1  44305  ssrecnpr  44332  seff  44333  sblpnf  44334  expgrowthi  44357  dvconstbi  44358  sumpair  45059  refsum2cnlem1  45061  iooinlbub  45530  elprn1  45662  elprn2  45663  cncfiooicclem1  45922  dvmptconst  45944  dvmptidg  45946  dvmulcncf  45954  dvdivcncf  45956  elprneb  47058  minusmodnep2tmod  47382  perfectALTVlem2  47736  grtriclwlk3  47957  gpgcubic  48081  gpg5nbgr3star  48083  gpgprismgr4cycllem3  48096  gpgprismgr4cycllem7  48100  gpgprismgr4cycllem10  48103  0dig2pr01  48590  prelrrx2b  48694  infsubc  49027  infsubc2  49028  setc2othin  49352