Theorem suppssdm 8202

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2108   ≠ wne 2940  {crab 3436  Vcvv 3480   ⊆ wss 3951  ∅c0 4333  {csn 4626  dom cdm 5685   “ cima 5688  (class class class)co 7431   supp csupp 8185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-supp 8186

This theorem is referenced by:  snopsuppss  8204  wemapso2lem  9592  cantnfcl  9707  cantnfle  9711  cantnflt  9712  cantnff  9714  cantnfres  9717  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  cantnflem3  9731  cnfcomlem  9739  cnfcom  9740  cnfcom3lem  9743  cnfcom3  9744  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  gsumval3lem1  19923  gsumval3lem2  19924  gsumval3  19925  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumconst  19952  gsumzoppg  19962  gsum2d  19990  dpjidcl  20078  gsumfsum  21452  regsumsupp  21640  frlmlbs  21817  psrass1lem  21952  psrass1  21984  psrass23l  21987  psrcom  21988  psrass23  21989  mplcoe1  22055  psropprmul  22239  coe1mul2  22272  tsmsgsum  24147  rrxcph  25426  rrxsuppss  25437  rrxmval  25439  mdegfval  26101  mdegleb  26103  mdegldg  26105  deg1mul3le  26156  wilthlem3  27113  suppovss  32690  fressupp  32697  ressupprn  32699  supppreima  32700  fsupprnfi  32701  fsuppcurry1  32736  fsuppcurry2  32737  gsumfs2d  33058  gsumhashmul  33064  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrspunidl  33456  rprmdvdsprod  33562  1arithidom  33565  fedgmullem1  33680  fldextrspunlsplem  33723  fldextrspunlsp  33724  zarcmplem  33880  fdivmpt  48461  fdivmptf  48462  refdivmptf  48463  fdivpm  48464  refdivpm  48465