Theorem suppssdm 8173

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 8158	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 4042	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3989	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 8159	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4364	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	eqsstrdi 3989	. 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
7	3, 6	pm2.61i 184	1 ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹

Syntax hints:  ¬ wn 3   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964  {crab 3423  Vcvv 3463   ⊆ wss 3913  ∅c0 4294  {csn 4594  dom cdm 5662   “ cima 5665  (class class class)co 7411   supp csupp 8156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-supp 8157

This theorem is referenced by:  snopsuppss  8175  wemapso2lem  9514  cantnfcl  9636  cantnfle  9640  cantnflt  9641  cantnff  9643  cantnfres  9646  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1  9658  cantnflem3  9660  cnfcomlem  9668  cnfcom  9669  cnfcom3lem  9672  cnfcom3  9673  fsuppmapnn0fiublem  14026  fsuppmapnn0fiub  14027  gsumval3lem1  19975  gsumval3lem2  19976  gsumval3  19977  gsumzres  19979  gsumzcl2  19980  gsumzf1o  19982  gsumzaddlem  19991  gsumconst  20004  gsumzoppg  20014  gsum2d  20042  dpjidcl  20130  gsumfsum  21553  regsumsupp  21741  frlmlbs  21916  psrass1lem  22052  psrass1  22082  psrass23l  22085  psrcom  22086  psrass23  22087  mplcoe1  22157  psropprmul  22366  coe1mul2  22399  tsmsgsum  24265  rrxcph  25520  rrxsuppss  25531  rrxmval  25533  mdegfval  26188  mdegleb  26190  mdegldg  26192  deg1mul3le  26243  wilthlem3  27200  suppovss  32967  fressupp  32974  ressupprn  32976  supppreima  32977  fsupprnfi  32978  fsuppcurry1  33010  fsuppcurry2  33011  gsumfs2d  33322  gsumhashmul  33328  elrgspnlem4  33506  elrgspnsubrunlem1  33508  elrgspnsubrunlem2  33509  elrspunidl  33680  rprmdvdsprod  33769  1arithidom  33772  esplymhp  33903  esplyfv1  33904  esplyfval3  33907  esplyfval1  33908  esplyfvaln  33909  esplyind  33910  fedgmullem1  33964  fldextrspunlsplem  34008  fldextrspunlsp  34009  zarcmplem  34216  fdivmpt  49205  fdivmptf  49206  refdivmptf  49207  fdivpm  49208  refdivpm  49209