Theorem suppssdm 8121

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 8106	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 4021	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3967	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 8107	. . 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 5625   “ cima 5628  (class class class)co 7361   supp csupp 8104

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 5232  ax-nul 5242  ax-pr 5371  ax-un 7683

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 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-supp 8105

This theorem is referenced by:  snopsuppss  8123  wemapso2lem  9461  cantnfcl  9582  cantnfle  9586  cantnflt  9587  cantnff  9589  cantnfres  9592  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1  9604  cantnflem3  9606  cnfcomlem  9614  cnfcom  9615  cnfcom3lem  9618  cnfcom3  9619  fsuppmapnn0fiublem  13946  fsuppmapnn0fiub  13947  gsumval3lem1  19874  gsumval3lem2  19875  gsumval3  19876  gsumzres  19878  gsumzcl2  19879  gsumzf1o  19881  gsumzaddlem  19890  gsumconst  19903  gsumzoppg  19913  gsum2d  19941  dpjidcl  20029  gsumfsum  21427  regsumsupp  21615  frlmlbs  21790  psrass1lem  21925  psrass1  21955  psrass23l  21958  psrcom  21959  psrass23  21960  mplcoe1  22028  psropprmul  22214  coe1mul2  22247  tsmsgsum  24117  rrxcph  25372  rrxsuppss  25383  rrxmval  25385  mdegfval  26040  mdegleb  26042  mdegldg  26044  deg1mul3le  26095  wilthlem3  27050  suppovss  32772  fressupp  32779  ressupprn  32781  supppreima  32782  fsupprnfi  32783  fsuppcurry1  32815  fsuppcurry2  32816  gsumfs2d  33140  gsumhashmul  33146  elrgspnlem4  33324  elrgspnsubrunlem1  33326  elrgspnsubrunlem2  33327  elrspunidl  33506  rprmdvdsprod  33612  1arithidom  33615  esplymhp  33730  esplyfv1  33731  esplyfval3  33734  esplyfval1  33735  esplyfvaln  33736  esplyind  33737  fedgmullem1  33792  fldextrspunlsplem  33836  fldextrspunlsp  33837  zarcmplem  34044  fdivmpt  49031  fdivmptf  49032  refdivmptf  49033  fdivpm  49034  refdivpm  49035