Theorem elpri 4600

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2111  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  elprn1  4604  elprn2  4605  nelpri  4608  nelprd  4610  tppreqb  4757  elpreqpr  4819  elpr2elpr  4821  prproe  4857  3elpr2eq  4858  opth1  5415  0nelop  5436  ftpg  7089  fvf1pr  7241  2oconcl  8418  cantnflem2  9580  eldju1st  9816  m1expcl2  13992  hash2pwpr  14383  bitsinv1lem  16352  prm23lt5  16726  fnpr2ob  17462  fvprif  17465  xpsfeq  17467  ex-chn2  18544  pmtrprfval  19400  m1expaddsub  19411  psgnprfval  19434  frgpuptinv  19684  frgpup3lem  19690  simpgnsgeqd  20016  2nsgsimpgd  20017  simpgnsgbid  20018  cnmsgnsubg  21515  zrhpsgnelbas  21532  mdetralt  22524  m2detleiblem1  22540  indiscld  23007  cnindis  23208  connclo  23331  txindis  23550  xpsxmetlem  24295  xpsmet  24298  ishl2  25298  recnprss  25833  recnperf  25834  dvlip2  25928  coseq0negpitopi  26440  pythag  26755  reasinsin  26834  scvxcvx  26924  perfectlem2  27169  lgslem4  27239  lgseisenlem2  27315  2lgsoddprmlem3  27353  usgredg4  29196  konigsberg  30235  ex-pr  30408  elpreq  32506  1neg1t1neg1  32719  tocyc01  33085  drngidl  33396  drng0mxidl  33439  ply1dg3rt0irred  33544  rtelextdg2  33738  constrconj  33756  signswch  34572  kur14lem7  35254  poimirlem31  37697  ftc1anclem2  37740  wepwsolem  43081  omabs2  43371  omcl3g  43373  relexp01min  43752  clsk1indlem1  44084  mnuprdlem1  44311  mnuprdlem2  44312  mnuprdlem3  44313  mnurndlem1  44320  ssrecnpr  44347  seff  44348  sblpnf  44349  expgrowthi  44372  dvconstbi  44373  sumpair  45078  refsum2cnlem1  45080  iooinlbub  45547  cncfiooicclem1  45937  dvmptconst  45959  dvmptidg  45961  dvmulcncf  45969  dvdivcncf  45971  elprneb  47066  minusmodnep2tmod  47390  perfectALTVlem2  47759  grtriclwlk3  47982  gpgcubic  48116  gpg5nbgr3star  48118  gpgprismgr4cycllem3  48134  gpgprismgr4cycllem7  48138  gpgprismgr4cycllem10  48141  pgnbgreunbgr  48162  0dig2pr01  48648  prelrrx2b  48752  infsubc  49098  infsubc2  49099  setc2othin  49504