Theorem fzsn 12939

Description: A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
fzsn	⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})

Proof of Theorem fzsn

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfz1eq 12908	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
2		elfz3 12907	. . . . 5 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀))
3		eleq1 2900	. . . . 5 ⊢ (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀)))
4	2, 3	syl5ibrcom 249	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑘 = 𝑀 → 𝑘 ∈ (𝑀...𝑀)))
5	1, 4	impbid2 228	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀))
6		velsn 4569	. . 3 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
7	5, 6	syl6bbr 291	. 2 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀}))
8	7	eqrdv 2819	1 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  {csn 4553  (class class class)co 7142  ℤcz 11968  ...cfz 12882

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-cnex 10579  ax-resscn 10580  ax-pre-lttri 10597  ax-pre-lttrn 10598

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-po 5460  df-so 5461  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ov 7145  df-oprab 7146  df-mpo 7147  df-1st 7675  df-2nd 7676  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-neg 10859  df-z 11969  df-uz 12231  df-fz 12883

This theorem is referenced by:  fzsuc  12944  fzpred  12945  fzpr  12952  fzsuc2  12955  fz0sn  12997  fz0sn0fz1  13014  fzosn  13098  seqf1o  13401  hashsng  13720  sumsnf  15084  fsum1  15087  fsumm1  15091  fsum1p  15093  prodsn  15301  fprod1  15302  prodsnf  15303  fprod1p  15307  fprodabs  15313  fprodefsum  15433  phi1  16093  vdwlem8  16307  strle1  16575  telgsumfzs  19092  pmatcollpw3fi1  21379  imasdsf1olem  22966  ehl1eudis  24006  voliunlem1  24134  ply1termlem  24779  pntpbnd1  26148  0wlkons1  27884  iuninc  30298  fzspl  30499  esumfzf  31335  ballotlemfc0  31757  ballotlemfcc  31758  plymulx0  31824  signstf0  31845  subfac1  32432  subfacp1lem1  32433  subfacp1lem5  32438  subfacp1lem6  32439  cvmliftlem10  32548  fwddifn0  33632  poimirlem2  34928  poimirlem3  34929  poimirlem4  34930  poimirlem6  34932  poimirlem7  34933  poimirlem13  34939  poimirlem14  34940  poimirlem16  34942  poimirlem17  34943  poimirlem18  34944  poimirlem19  34945  poimirlem20  34946  poimirlem21  34947  poimirlem22  34948  poimirlem26  34952  poimirlem28  34954  poimirlem31  34957  poimirlem32  34958  sdclem1  35050  fdc  35052  trclfvdecomr  40163  k0004val0  40594  sumsnd  41373  fzdifsuc2  41667  dvnmul  42318  stoweidlem17  42392  carageniuncllem1  42893  caratheodorylem1  42898  hoidmvlelem3  42969  fzopredsuc  43613  sbgoldbo  44037  nnsum3primesprm  44040