Theorem suppssdm 7919

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 7905	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 3993	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3955	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 7906	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4311	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	eqsstrdi 3955	. 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
7	3, 6	pm2.61i 185	1 ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹

Syntax hints:  ¬ wn 3   ∧ wa 399   ∈ wcel 2110   ≠ wne 2940  {crab 3065  Vcvv 3408   ⊆ wss 3866  ∅c0 4237  {csn 4541  dom cdm 5551   “ cima 5554  (class class class)co 7213   supp csupp 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-supp 7904

This theorem is referenced by:  snopsuppss  7921  wemapso2lem  9168  cantnfcl  9282  cantnfle  9286  cantnflt  9287  cantnff  9289  cantnfres  9292  cantnfp1lem3  9295  cantnflem1b  9301  cantnflem1  9304  cantnflem3  9306  cnfcomlem  9314  cnfcom  9315  cnfcom3lem  9318  cnfcom3  9319  fsuppmapnn0fiublem  13563  fsuppmapnn0fiub  13564  gsumval3lem1  19290  gsumval3lem2  19291  gsumval3  19292  gsumzres  19294  gsumzcl2  19295  gsumzf1o  19297  gsumzaddlem  19306  gsumconst  19319  gsumzoppg  19329  gsum2d  19357  dpjidcl  19445  gsumfsum  20430  regsumsupp  20584  frlmlbs  20759  psrass1lemOLD  20899  psrass1lem  20902  psrass1  20930  psrass23l  20933  psrcom  20934  psrass23  20935  mplcoe1  20994  psropprmul  21159  coe1mul2  21190  tsmsgsum  23036  rrxcph  24289  rrxsuppss  24300  rrxmval  24302  mdegfval  24960  mdegleb  24962  mdegldg  24964  deg1mul3le  25014  wilthlem3  25952  suppovss  30737  fressupp  30742  ressupprn  30744  supppreima  30745  fsupprnfi  30746  fsuppcurry1  30780  fsuppcurry2  30781  gsumhashmul  31035  elrspunidl  31320  fedgmullem1  31424  zarcmplem  31545  fdivmpt  45559  fdivmptf  45560  refdivmptf  45561  fdivpm  45562  refdivpm  45563