Theorem fzsn 13594

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 13563	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
2		elfz3 13562	. . . . 5 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀))
3		eleq1 2857	. . . . 5 ⊢ (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀)))
4	2, 3	syl5ibrcom 250	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑘 = 𝑀 → 𝑘 ∈ (𝑀...𝑀)))
5	1, 4	impbid2 229	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀))
6		velsn 4608	. . 3 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀}))
8	7	eqrdv 2767	1 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {csn 4592  (class class class)co 7411  ℤcz 12591  ...cfz 13535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-pre-lttri 11174  ax-pre-lttrn 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-neg 11444  df-z 12592  df-uz 12863  df-fz 13536

This theorem is referenced by:  fzsuc  13599  fzpred  13600  fzpr  13607  fzsuc2  13610  fz0sn  13655  fz0sn0fz1  13673  fzosn  13765  seqf1o  14079  hashsng  14405  sumsnf  15794  fsum1  15798  fsumm1  15802  fsum1p  15804  prodsn  16016  fprod1  16017  prodsnf  16018  fprod1p  16022  fprodabs  16028  fprodefsum  16149  phi1  16832  vdwlem8  17048  strle1  17218  telgsumfzs  20059  pmatcollpw3fi1  22914  imasdsf1olem  24499  ehl1eudis  25548  voliunlem1  25678  ply1termlem  26329  plyn0mulidp  26411  pntpbnd1  27716  0wlkons1  30413  iuninc  32846  fzspl  33075  esumfzf  34404  ballotlemfc0  34828  ballotlemfcc  34829  signstf0  34900  subfac1  35603  subfacp1lem1  35604  subfacp1lem5  35609  subfacp1lem6  35610  cvmliftlem10  35719  fwddifn0  36589  poimirlem2  38196  poimirlem3  38197  poimirlem4  38198  poimirlem6  38200  poimirlem7  38201  poimirlem13  38207  poimirlem14  38208  poimirlem16  38210  poimirlem17  38211  poimirlem18  38212  poimirlem19  38213  poimirlem20  38214  poimirlem21  38215  poimirlem22  38216  poimirlem26  38220  poimirlem28  38222  poimirlem31  38225  poimirlem32  38226  sdclem1  38317  fdc  38319  aks6d1c1  42808  sticksstones9  42846  sticksstones11  42848  trclfvdecomr  44381  k0004val0  44807  sumsnd  45673  fzdifsuc2  45956  dvnmul  46584  stoweidlem17  46658  carageniuncllem1  47162  caratheodorylem1  47167  hoidmvlelem3  47238  fzopredsuc  47985  sbgoldbo  48476  nnsum3primesprm  48479  stgr1  48650