Theorem suppssdm 8232

Description: The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.)

Assertion

Ref	Expression
suppssdm	⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹

Proof of Theorem suppssdm

Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		suppval 8216	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 4008	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3957	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 8217	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4353	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	eqsstrdi 3957	. 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
7	3, 6	pm2.61i 184	1 ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∈ wcel 2147   ≠ wne 2959  {crab 3416  Vcvv 3454   ⊆ wss 3900  ∅c0 4281  {csn 4588  dom cdm 5658   “ cima 5661  (class class class)co 7451   supp csupp 8214

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-supp 8215

This theorem is used by:  snopsuppss  8234  wemapso2lem  9583  cantnfcl  9705  cantnfle  9709  cantnflt  9710  cantnff  9712  cantnfres  9715  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1  9727  cantnflem3  9729  cnfcomlem  9737  cnfcom  9738  cnfcom3lem  9741  cnfcom3  9742  fsuppmapnn0fiublem  14173  fsuppmapnn0fiub  14174  gsumval3lem1  20170  gsumval3lem2  20171  gsumval3  20172  gsumzres  20174  gsumzcl2  20175  gsumzf1o  20177  gsumzaddlem  20186  gsumconst  20199  gsumzoppg  20209  gsum2d  20237  dpjidcl  20325  gsumfsum  21794  regsumsupp  21983  frlmlbs  22158  psrass1lem  22296  psrass1  22326  psrass23l  22329  psrcom  22330  psrass23  22331  mplcoe1  22401  psropprmul  22610  coe1mul2  22643  tsmsgsum  24513  rrxcph  25768  rrxsuppss  25779  rrxmval  25781  mdegfval  26435  mdegleb  26437  mdegldg  26439  deg1mul3le  26490  wilthlem3  27454  suppovss  33371  fressupp  33378  ressupprn  33380  supppreima  33381  fsupprnfi  33382  fsuppcurry1  33412  fsuppcurry2  33413  gsumfs2d  33721  gsumhashmul  33727  elrgspnlem4  33905  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  elrspunidl  34082  rprmdvdsprod  34170  1arithidom  34173  esplymhp  34311  esplyfv1  34312  esplyfval3  34315  esplyfval1  34316  esplyfvaln  34317  esplyind  34318  fedgmullem1  34372  fldextrspunlsplem  34416  fldextrspunlsp  34417  zarcmplem  34624  fdivmpt  49983  fdivmptf  49984  refdivmptf  49985  fdivpm  49986  refdivpm  49987