Theorem elpri 4606

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  elprn1  4610  elprn2  4611  nelpri  4614  nelprd  4616  tppreqb  4763  elpreqpr  4825  elpr2elpr  4827  prproe  4863  3elpr2eq  4864  opth1  5431  0nelop  5452  ftpg  7111  fvf1pr  7263  2oconcl  8440  cantnflem2  9611  eldju1st  9847  m1expcl2  14020  hash2pwpr  14411  bitsinv1lem  16380  prm23lt5  16754  fnpr2ob  17491  fvprif  17494  xpsfeq  17496  ex-chn2  18573  pmtrprfval  19428  m1expaddsub  19439  psgnprfval  19462  frgpuptinv  19712  frgpup3lem  19718  simpgnsgeqd  20044  2nsgsimpgd  20045  simpgnsgbid  20046  cnmsgnsubg  21544  zrhpsgnelbas  21561  mdetralt  22564  m2detleiblem1  22580  indiscld  23047  cnindis  23248  connclo  23371  txindis  23590  xpsxmetlem  24335  xpsmet  24338  ishl2  25338  recnprss  25873  recnperf  25874  dvlip2  25968  coseq0negpitopi  26480  pythag  26795  reasinsin  26874  scvxcvx  26964  perfectlem2  27209  lgslem4  27279  lgseisenlem2  27355  2lgsoddprmlem3  27393  usgredg4  29302  konigsberg  30344  ex-pr  30517  elpreq  32614  1neg1t1neg1  32827  tocyc01  33211  drngidl  33525  drng0mxidl  33568  ply1dg3rt0irred  33676  rtelextdg2  33904  constrconj  33922  signswch  34738  kur14lem7  35425  poimirlem31  37899  ftc1anclem2  37942  wepwsolem  43396  omabs2  43686  omcl3g  43688  relexp01min  44066  clsk1indlem1  44398  mnuprdlem1  44625  mnuprdlem2  44626  mnuprdlem3  44627  mnurndlem1  44634  ssrecnpr  44661  seff  44662  sblpnf  44663  expgrowthi  44686  dvconstbi  44687  sumpair  45392  refsum2cnlem1  45394  iooinlbub  45858  cncfiooicclem1  46248  dvmptconst  46270  dvmptidg  46272  dvmulcncf  46280  dvdivcncf  46282  elprneb  47386  minusmodnep2tmod  47710  perfectALTVlem2  48079  grtriclwlk3  48302  gpgcubic  48436  gpg5nbgr3star  48438  gpgprismgr4cycllem3  48454  gpgprismgr4cycllem7  48458  gpgprismgr4cycllem10  48461  pgnbgreunbgr  48482  0dig2pr01  48967  prelrrx2b  49071  infsubc  49416  infsubc2  49417  setc2othin  49822