Theorem suppssdm 8117

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 8102	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 4030	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3976	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 8103	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4350	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	eqsstrdi 3976	. 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
7	3, 6	pm2.61i 182	1 ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2113   ≠ wne 2930  {crab 3397  Vcvv 3438   ⊆ wss 3899  ∅c0 4283  {csn 4578  dom cdm 5622   “ cima 5625  (class class class)co 7356   supp csupp 8100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-supp 8101

This theorem is referenced by:  snopsuppss  8119  wemapso2lem  9455  cantnfcl  9574  cantnfle  9578  cantnflt  9579  cantnff  9581  cantnfres  9584  cantnfp1lem3  9587  cantnflem1b  9593  cantnflem1  9596  cantnflem3  9598  cnfcomlem  9606  cnfcom  9607  cnfcom3lem  9610  cnfcom3  9611  fsuppmapnn0fiublem  13911  fsuppmapnn0fiub  13912  gsumval3lem1  19832  gsumval3lem2  19833  gsumval3  19834  gsumzres  19836  gsumzcl2  19837  gsumzf1o  19839  gsumzaddlem  19848  gsumconst  19861  gsumzoppg  19871  gsum2d  19899  dpjidcl  19987  gsumfsum  21387  regsumsupp  21575  frlmlbs  21750  psrass1lem  21886  psrass1  21917  psrass23l  21920  psrcom  21921  psrass23  21922  mplcoe1  21990  psropprmul  22176  coe1mul2  22209  tsmsgsum  24081  rrxcph  25346  rrxsuppss  25357  rrxmval  25359  mdegfval  26021  mdegleb  26023  mdegldg  26025  deg1mul3le  26076  wilthlem3  27034  suppovss  32709  fressupp  32716  ressupprn  32718  supppreima  32719  fsupprnfi  32720  fsuppcurry1  32752  fsuppcurry2  32753  gsumfs2d  33093  gsumhashmul  33099  elrgspnlem4  33276  elrgspnsubrunlem1  33278  elrgspnsubrunlem2  33279  elrspunidl  33458  rprmdvdsprod  33564  1arithidom  33567  esplymhp  33675  esplyfv1  33676  esplyfval3  33679  esplyind  33680  fedgmullem1  33735  fldextrspunlsplem  33779  fldextrspunlsp  33780  zarcmplem  33987  fdivmpt  48728  fdivmptf  48729  refdivmptf  48730  fdivpm  48731  refdivpm  48732