Theorem fzsn 13601

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 13569	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
2		elfz3 13568	. . . . 5 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀))
3		eleq1 2850	. . . . 5 ⊢ (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀)))
4	2, 3	syl5ibrcom 250	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑘 = 𝑀 → 𝑘 ∈ (𝑀...𝑀)))
5	1, 4	impbid2 229	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀))
6		velsn 4604	. . 3 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀}))
8	7	eqrdv 2760	1 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  {csn 4588  (class class class)co 7412  ℤcz 12597  ...cfz 13541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-po 5568  df-so 5569  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7984  df-2nd 7985  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-neg 11450  df-z 12598  df-uz 12869  df-fz 13542

This theorem is used by:  fzsuc  13606  fzpred  13607  fzpr  13614  fzsuc2  13617  fz0sn  13662  fz0sn0fz1  13680  fzosn  13772  seqf1o  14086  hashsng  14412  sumsnf  15801  fsum1  15805  fsumm1  15809  fsum1p  15811  prodsn  16023  fprod1  16024  prodsnf  16025  fprod1p  16029  fprodabs  16035  fprodefsum  16155  phi1  16838  vdwlem8  17054  strle1  17224  telgsumfzs  20065  pmatcollpw3fi1  22956  imasdsf1olem  24541  ehl1eudis  25590  voliunlem1  25720  ply1termlem  26371  plyn0mulidp  26453  pntpbnd1  27761  0wlkons1  30483  iuninc  32916  fzspl  33145  esumfzf  34468  ballotlemfc0  34892  ballotlemfcc  34893  signstf0  34964  subfac1  35678  subfacp1lem1  35679  subfacp1lem5  35684  subfacp1lem6  35685  cvmliftlem10  35794  fwddifn0  36664  poimirlem2  38301  poimirlem3  38302  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem13  38312  poimirlem14  38313  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem26  38325  poimirlem28  38327  poimirlem31  38330  poimirlem32  38331  sdclem1  38422  fdc  38424  aks6d1c1  42911  sticksstones9  42949  sticksstones11  42951  trclfvdecomr  44482  k0004val0  44908  sumsnd  45774  fzdifsuc2  46057  dvnmul  46685  stoweidlem17  46759  carageniuncllem1  47263  caratheodorylem1  47268  hoidmvlelem3  47339  fzopredsuc  48089  sbgoldbo  48580  nnsum3primesprm  48583  stgr1  48754