Theorem suppssdm 8107

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2111   ≠ wne 2928  {crab 3395  Vcvv 3436   ⊆ wss 3897  ∅c0 4280  {csn 4573  dom cdm 5614   “ cima 5617  (class class class)co 7346   supp csupp 8090

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-supp 8091

This theorem is referenced by:  snopsuppss  8109  wemapso2lem  9438  cantnfcl  9557  cantnfle  9561  cantnflt  9562  cantnff  9564  cantnfres  9567  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1  9579  cantnflem3  9581  cnfcomlem  9589  cnfcom  9590  cnfcom3lem  9593  cnfcom3  9594  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  gsumval3lem1  19817  gsumval3lem2  19818  gsumval3  19819  gsumzres  19821  gsumzcl2  19822  gsumzf1o  19824  gsumzaddlem  19833  gsumconst  19846  gsumzoppg  19856  gsum2d  19884  dpjidcl  19972  gsumfsum  21371  regsumsupp  21559  frlmlbs  21734  psrass1lem  21869  psrass1  21901  psrass23l  21904  psrcom  21905  psrass23  21906  mplcoe1  21972  psropprmul  22150  coe1mul2  22183  tsmsgsum  24054  rrxcph  25319  rrxsuppss  25330  rrxmval  25332  mdegfval  25994  mdegleb  25996  mdegldg  25998  deg1mul3le  26049  wilthlem3  27007  suppovss  32662  fressupp  32669  ressupprn  32671  supppreima  32672  fsupprnfi  32673  fsuppcurry1  32707  fsuppcurry2  32708  gsumfs2d  33035  gsumhashmul  33041  elrgspnlem4  33212  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  elrspunidl  33393  rprmdvdsprod  33499  1arithidom  33502  esplymhp  33589  esplyfv1  33590  fedgmullem1  33642  fldextrspunlsplem  33686  fldextrspunlsp  33687  zarcmplem  33894  fdivmpt  48651  fdivmptf  48652  refdivmptf  48653  fdivpm  48654  refdivpm  48655