Theorem suppssdm 8120

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933  {crab 3390  Vcvv 3430   ⊆ wss 3890  ∅c0 4274  {csn 4568  dom cdm 5624   “ cima 5627  (class class class)co 7360   supp csupp 8103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-supp 8104

This theorem is referenced by:  snopsuppss  8122  wemapso2lem  9460  cantnfcl  9579  cantnfle  9583  cantnflt  9584  cantnff  9586  cantnfres  9589  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1  9601  cantnflem3  9603  cnfcomlem  9611  cnfcom  9612  cnfcom3lem  9615  cnfcom3  9616  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  gsumval3lem1  19871  gsumval3lem2  19872  gsumval3  19873  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumconst  19900  gsumzoppg  19910  gsum2d  19938  dpjidcl  20026  gsumfsum  21424  regsumsupp  21612  frlmlbs  21787  psrass1lem  21922  psrass1  21952  psrass23l  21955  psrcom  21956  psrass23  21957  mplcoe1  22025  psropprmul  22211  coe1mul2  22244  tsmsgsum  24114  rrxcph  25369  rrxsuppss  25380  rrxmval  25382  mdegfval  26037  mdegleb  26039  mdegldg  26041  deg1mul3le  26092  wilthlem3  27047  suppovss  32769  fressupp  32776  ressupprn  32778  supppreima  32779  fsupprnfi  32780  fsuppcurry1  32812  fsuppcurry2  32813  gsumfs2d  33137  gsumhashmul  33143  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrspunidl  33503  rprmdvdsprod  33609  1arithidom  33612  esplymhp  33727  esplyfv1  33728  esplyfval3  33731  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  fedgmullem1  33789  fldextrspunlsplem  33833  fldextrspunlsp  33834  zarcmplem  34041  fdivmpt  49028  fdivmptf  49029  refdivmptf  49030  fdivpm  49031  refdivpm  49032