Theorem fzsn 13469

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 13438	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
2		elfz3 13437	. . . . 5 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀))
3		eleq1 2816	. . . . 5 ⊢ (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀)))
4	2, 3	syl5ibrcom 247	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑘 = 𝑀 → 𝑘 ∈ (𝑀...𝑀)))
5	1, 4	impbid2 226	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀))
6		velsn 4593	. . 3 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
7	5, 6	bitr4di 289	. 2 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀}))
8	7	eqrdv 2727	1 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {csn 4577  (class class class)co 7349  ℤcz 12471  ...cfz 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-pre-lttri 11083  ax-pre-lttrn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-1st 7924  df-2nd 7925  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-neg 11350  df-z 12472  df-uz 12736  df-fz 13411

This theorem is referenced by:  fzsuc  13474  fzpred  13475  fzpr  13482  fzsuc2  13485  fz0sn  13530  fz0sn0fz1  13548  fzosn  13639  seqf1o  13950  hashsng  14276  sumsnf  15650  fsum1  15654  fsumm1  15658  fsum1p  15660  prodsn  15869  fprod1  15870  prodsnf  15871  fprod1p  15875  fprodabs  15881  fprodefsum  16002  phi1  16684  vdwlem8  16900  strle1  17069  telgsumfzs  19868  pmatcollpw3fi1  22673  imasdsf1olem  24259  ehl1eudis  25318  voliunlem1  25449  ply1termlem  26106  pntpbnd1  27495  0wlkons1  30069  iuninc  32509  fzspl  32741  esumfzf  34052  ballotlemfc0  34477  ballotlemfcc  34478  plymulx0  34531  signstf0  34552  subfac1  35171  subfacp1lem1  35172  subfacp1lem5  35177  subfacp1lem6  35178  cvmliftlem10  35287  fwddifn0  36158  poimirlem2  37622  poimirlem3  37623  poimirlem4  37624  poimirlem6  37626  poimirlem7  37627  poimirlem13  37633  poimirlem14  37634  poimirlem16  37636  poimirlem17  37637  poimirlem18  37638  poimirlem19  37639  poimirlem20  37640  poimirlem21  37641  poimirlem22  37642  poimirlem26  37646  poimirlem28  37648  poimirlem31  37651  poimirlem32  37652  sdclem1  37743  fdc  37745  aks6d1c1  42109  sticksstones9  42147  sticksstones11  42149  trclfvdecomr  43721  k0004val0  44147  sumsnd  45024  fzdifsuc2  45312  dvnmul  45944  stoweidlem17  46018  carageniuncllem1  46522  caratheodorylem1  46527  hoidmvlelem3  46598  fzopredsuc  47327  sbgoldbo  47791  nnsum3primesprm  47794  stgr1  47965