Theorem suppssdm 8159

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2109   ≠ wne 2926  {crab 3408  Vcvv 3450   ⊆ wss 3917  ∅c0 4299  {csn 4592  dom cdm 5641   “ cima 5644  (class class class)co 7390   supp csupp 8142

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-supp 8143

This theorem is referenced by:  snopsuppss  8161  wemapso2lem  9512  cantnfcl  9627  cantnfle  9631  cantnflt  9632  cantnff  9634  cantnfres  9637  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  cantnflem3  9651  cnfcomlem  9659  cnfcom  9660  cnfcom3lem  9663  cnfcom3  9664  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  gsumval3lem1  19842  gsumval3lem2  19843  gsumval3  19844  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumconst  19871  gsumzoppg  19881  gsum2d  19909  dpjidcl  19997  gsumfsum  21358  regsumsupp  21538  frlmlbs  21713  psrass1lem  21848  psrass1  21880  psrass23l  21883  psrcom  21884  psrass23  21885  mplcoe1  21951  psropprmul  22129  coe1mul2  22162  tsmsgsum  24033  rrxcph  25299  rrxsuppss  25310  rrxmval  25312  mdegfval  25974  mdegleb  25976  mdegldg  25978  deg1mul3le  26029  wilthlem3  26987  suppovss  32611  fressupp  32618  ressupprn  32620  supppreima  32621  fsupprnfi  32622  fsuppcurry1  32655  fsuppcurry2  32656  gsumfs2d  33002  gsumhashmul  33008  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrspunidl  33406  rprmdvdsprod  33512  1arithidom  33515  fedgmullem1  33632  fldextrspunlsplem  33675  fldextrspunlsp  33676  zarcmplem  33878  fdivmpt  48533  fdivmptf  48534  refdivmptf  48535  fdivpm  48536  refdivpm  48537