Theorem fzsn 13700

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 13668	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
2		elfz3 13667	. . . . 5 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀))
3		eleq1 2848	. . . . 5 ⊢ (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀)))
4	2, 3	syl5ibrcom 250	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑘 = 𝑀 → 𝑘 ∈ (𝑀...𝑀)))
5	1, 4	impbid2 229	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀))
6		velsn 4599	. . 3 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀}))
8	7	eqrdv 2758	1 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {csn 4583  (class class class)co 7420  ℤcz 12693  ...cfz 13639

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-pre-lttri 11274  ax-pre-lttrn 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-neg 11544  df-z 12694  df-uz 12966  df-fz 13640

This theorem is used by:  fzsuc  13705  fzpred  13706  fzpr  13713  fzsuc2  13716  fz0sn  13761  fz0sn0fz1  13779  fzosn  13871  seqf1o  14186  hashsng  14513  sumsnf  15909  fsum1  15913  fsumm1  15917  fsum1p  15919  prodsn  16129  fprod1  16130  prodsnf  16131  fprod1p  16135  fprodabs  16141  fprodefsum  16261  phi1  16950  vdwlem8  17166  strle1  17336  telgsumfzs  20203  pmatcollpw3fi1  23106  imasdsf1olem  24692  ehl1eudis  25741  voliunlem1  25871  ply1termlem  26521  plyn0mulidp  26602  pntpbnd1  27913  0wlkons1  30712  iuninc  33155  fzspl  33381  esumfzf  34701  ballotlemfc0  35125  ballotlemfcc  35126  signstf0  35197  subfac1  35943  subfacp1lem1  35944  subfacp1lem5  35949  subfacp1lem6  35950  cvmliftlem10  36059  fwddifn0  36929  poimirlem2  38541  poimirlem3  38542  poimirlem4  38543  poimirlem6  38545  poimirlem7  38546  poimirlem13  38552  poimirlem14  38553  poimirlem16  38555  poimirlem17  38556  poimirlem18  38557  poimirlem19  38558  poimirlem20  38559  poimirlem21  38560  poimirlem22  38561  poimirlem26  38565  poimirlem28  38567  poimirlem31  38570  poimirlem32  38571  sdclem1  38678  fdc  38680  aks6d1c1  43167  sticksstones9  43205  sticksstones11  43207  trclfvdecomr  44728  k0004val0  45154  sumsnd  46043  fzdifsuc2  46326  dvnmul  46953  stoweidlem17  47027  carageniuncllem1  47531  caratheodorylem1  47536  hoidmvlelem3  47607  fzopredsuc  48394  sbgoldbo  48885  nnsum3primesprm  48888  stgr1  49059