Theorem suppssdm 8068

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

Syntax hints:  ¬ wn 3   ∧ wa 397   ∈ wcel 2106   ≠ wne 2941  {crab 3404  Vcvv 3442   ⊆ wss 3902  ∅c0 4274  {csn 4578  dom cdm 5625   “ cima 5628  (class class class)co 7342   supp csupp 8052

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pr 5377  ax-un 7655

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3732  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-opab 5160  df-id 5523  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 6436  df-fun 6486  df-fv 6492  df-ov 7345  df-oprab 7346  df-mpo 7347  df-supp 8053

This theorem is referenced by:  snopsuppss  8070  wemapso2lem  9414  cantnfcl  9529  cantnfle  9533  cantnflt  9534  cantnff  9536  cantnfres  9539  cantnfp1lem3  9542  cantnflem1b  9548  cantnflem1  9551  cantnflem3  9553  cnfcomlem  9561  cnfcom  9562  cnfcom3lem  9565  cnfcom3  9566  fsuppmapnn0fiublem  13816  fsuppmapnn0fiub  13817  gsumval3lem1  19601  gsumval3lem2  19602  gsumval3  19603  gsumzres  19605  gsumzcl2  19606  gsumzf1o  19608  gsumzaddlem  19617  gsumconst  19630  gsumzoppg  19640  gsum2d  19668  dpjidcl  19756  gsumfsum  20771  regsumsupp  20933  frlmlbs  21110  psrass1lemOLD  21249  psrass1lem  21252  psrass1  21280  psrass23l  21283  psrcom  21284  psrass23  21285  mplcoe1  21344  psropprmul  21515  coe1mul2  21546  tsmsgsum  23396  rrxcph  24662  rrxsuppss  24673  rrxmval  24675  mdegfval  25333  mdegleb  25335  mdegldg  25337  deg1mul3le  25387  wilthlem3  26325  suppovss  31302  fressupp  31307  ressupprn  31309  supppreima  31310  fsupprnfi  31311  fsuppcurry1  31345  fsuppcurry2  31346  gsumhashmul  31601  elrspunidl  31901  fedgmullem1  32006  zarcmplem  32127  fdivmpt  46302  fdivmptf  46303  refdivmptf  46304  fdivpm  46305  refdivpm  46306