Theorem suppssdm 8129

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933  {crab 3401  Vcvv 3442   ⊆ wss 3903  ∅c0 4287  {csn 4582  dom cdm 5632   “ cima 5635  (class class class)co 7368   supp csupp 8112

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-supp 8113

This theorem is referenced by:  snopsuppss  8131  wemapso2lem  9469  cantnfcl  9588  cantnfle  9592  cantnflt  9593  cantnff  9595  cantnfres  9598  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  cantnflem3  9612  cnfcomlem  9620  cnfcom  9621  cnfcom3lem  9624  cnfcom3  9625  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  gsumval3lem1  19846  gsumval3lem2  19847  gsumval3  19848  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumconst  19875  gsumzoppg  19885  gsum2d  19913  dpjidcl  20001  gsumfsum  21401  regsumsupp  21589  frlmlbs  21764  psrass1lem  21900  psrass1  21931  psrass23l  21934  psrcom  21935  psrass23  21936  mplcoe1  22004  psropprmul  22190  coe1mul2  22223  tsmsgsum  24095  rrxcph  25360  rrxsuppss  25371  rrxmval  25373  mdegfval  26035  mdegleb  26037  mdegldg  26039  deg1mul3le  26090  wilthlem3  27048  suppovss  32771  fressupp  32778  ressupprn  32780  supppreima  32781  fsupprnfi  32782  fsuppcurry1  32814  fsuppcurry2  32815  gsumfs2d  33155  gsumhashmul  33161  elrgspnlem4  33339  elrgspnsubrunlem1  33341  elrgspnsubrunlem2  33342  elrspunidl  33521  rprmdvdsprod  33627  1arithidom  33630  esplymhp  33745  esplyfv1  33746  esplyfval3  33749  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  fedgmullem1  33807  fldextrspunlsplem  33851  fldextrspunlsp  33852  zarcmplem  34059  fdivmpt  48900  fdivmptf  48901  refdivmptf  48902  fdivpm  48903  refdivpm  48904