Theorem suppssdm 8218

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2108   ≠ wne 2946  {crab 3443  Vcvv 3488   ⊆ wss 3976  ∅c0 4352  {csn 4648  dom cdm 5700   “ cima 5703  (class class class)co 7448   supp csupp 8201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-supp 8202

This theorem is referenced by:  snopsuppss  8220  wemapso2lem  9621  cantnfcl  9736  cantnfle  9740  cantnflt  9741  cantnff  9743  cantnfres  9746  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1  9758  cantnflem3  9760  cnfcomlem  9768  cnfcom  9769  cnfcom3lem  9772  cnfcom3  9773  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  gsumval3lem1  19947  gsumval3lem2  19948  gsumval3  19949  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzoppg  19986  gsum2d  20014  dpjidcl  20102  gsumfsum  21475  regsumsupp  21663  frlmlbs  21840  psrass1lem  21975  psrass1  22007  psrass23l  22010  psrcom  22011  psrass23  22012  mplcoe1  22078  psropprmul  22260  coe1mul2  22293  tsmsgsum  24168  rrxcph  25445  rrxsuppss  25456  rrxmval  25458  mdegfval  26121  mdegleb  26123  mdegldg  26125  deg1mul3le  26176  wilthlem3  27131  suppovss  32697  fressupp  32700  ressupprn  32702  supppreima  32703  fsupprnfi  32704  fsuppcurry1  32739  fsuppcurry2  32740  gsumhashmul  33040  elrspunidl  33421  rprmdvdsprod  33527  1arithidom  33530  fedgmullem1  33642  zarcmplem  33827  fdivmpt  48274  fdivmptf  48275  refdivmptf  48276  fdivpm  48277  refdivpm  48278