Theorem suppssdm 8157

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 8142	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 4033	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3980	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 8143	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4354	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	eqsstrdi 3980	. 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
7	3, 6	pm2.61i 183	1 ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹

Syntax hints:  ¬ wn 3   ∧ wa 399   ∈ wcel 2142   ≠ wne 2957  {crab 3414  Vcvv 3454   ⊆ wss 3904  ∅c0 4285  {csn 4582  dom cdm 5647   “ cima 5650  (class class class)co 7396   supp csupp 8140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-supp 8141

This theorem is referenced by:  snopsuppss  8159  wemapso2lem  9500  cantnfcl  9622  cantnfle  9626  cantnflt  9627  cantnff  9629  cantnfres  9632  cantnfp1lem3  9635  cantnflem1b  9641  cantnflem1  9644  cantnflem3  9646  cnfcomlem  9654  cnfcom  9655  cnfcom3lem  9658  cnfcom3  9659  fsuppmapnn0fiublem  14003  fsuppmapnn0fiub  14004  gsumval3lem1  19945  gsumval3lem2  19946  gsumval3  19947  gsumzres  19949  gsumzcl2  19950  gsumzf1o  19952  gsumzaddlem  19961  gsumconst  19974  gsumzoppg  19984  gsum2d  20012  dpjidcl  20100  gsumfsum  21486  regsumsupp  21674  frlmlbs  21849  psrass1lem  21985  psrass1  22015  psrass23l  22018  psrcom  22019  psrass23  22020  mplcoe1  22090  psropprmul  22299  coe1mul2  22332  tsmsgsum  24199  rrxcph  25454  rrxsuppss  25465  rrxmval  25467  mdegfval  26122  mdegleb  26124  mdegldg  26126  deg1mul3le  26177  wilthlem3  27134  suppovss  32883  fressupp  32890  ressupprn  32892  supppreima  32893  fsupprnfi  32894  fsuppcurry1  32926  fsuppcurry2  32927  gsumfs2d  33241  gsumhashmul  33247  elrgspnlem4  33426  elrgspnsubrunlem1  33428  elrgspnsubrunlem2  33429  elrspunidl  33614  rprmdvdsprod  33730  1arithidom  33733  esplymhp  33865  esplyfv1  33866  esplyfval3  33869  esplyfval1  33870  esplyfvaln  33871  esplyind  33872  fedgmullem1  33926  fldextrspunlsplem  33970  fldextrspunlsp  33971  zarcmplem  34178  fdivmpt  49162  fdivmptf  49163  refdivmptf  49164  fdivpm  49165  refdivpm  49166