Theorem suppssdm 7993

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

Syntax hints:  ¬ wn 3   ∧ wa 396   ∈ wcel 2106   ≠ wne 2943  {crab 3068  Vcvv 3432   ⊆ wss 3887  ∅c0 4256  {csn 4561  dom cdm 5589   “ cima 5592  (class class class)co 7275   supp csupp 7977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-supp 7978

This theorem is referenced by:  snopsuppss  7995  wemapso2lem  9311  cantnfcl  9425  cantnfle  9429  cantnflt  9430  cantnff  9432  cantnfres  9435  cantnfp1lem3  9438  cantnflem1b  9444  cantnflem1  9447  cantnflem3  9449  cnfcomlem  9457  cnfcom  9458  cnfcom3lem  9461  cnfcom3  9462  fsuppmapnn0fiublem  13710  fsuppmapnn0fiub  13711  gsumval3lem1  19506  gsumval3lem2  19507  gsumval3  19508  gsumzres  19510  gsumzcl2  19511  gsumzf1o  19513  gsumzaddlem  19522  gsumconst  19535  gsumzoppg  19545  gsum2d  19573  dpjidcl  19661  gsumfsum  20665  regsumsupp  20827  frlmlbs  21004  psrass1lemOLD  21143  psrass1lem  21146  psrass1  21174  psrass23l  21177  psrcom  21178  psrass23  21179  mplcoe1  21238  psropprmul  21409  coe1mul2  21440  tsmsgsum  23290  rrxcph  24556  rrxsuppss  24567  rrxmval  24569  mdegfval  25227  mdegleb  25229  mdegldg  25231  deg1mul3le  25281  wilthlem3  26219  suppovss  31017  fressupp  31022  ressupprn  31024  supppreima  31025  fsupprnfi  31026  fsuppcurry1  31060  fsuppcurry2  31061  gsumhashmul  31316  elrspunidl  31606  fedgmullem1  31710  zarcmplem  31831  fdivmpt  45886  fdivmptf  45887  refdivmptf  45888  fdivpm  45889  refdivpm  45890