Theorem suppssdm 8179

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

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∈ wcel 2146   ≠ wne 2960  {crab 3418  Vcvv 3457   ⊆ wss 3906  ∅c0 4286  {csn 4591  dom cdm 5663   “ cima 5666  (class class class)co 7419   supp csupp 8162

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-supp 8163

This theorem is used by:  snopsuppss  8181  wemapso2lem  9521  cantnfcl  9643  cantnfle  9647  cantnflt  9648  cantnff  9650  cantnfres  9653  cantnfp1lem3  9656  cantnflem1b  9662  cantnflem1  9665  cantnflem3  9667  cnfcomlem  9675  cnfcom  9676  cnfcom3lem  9679  cnfcom3  9680  fsuppmapnn0fiublem  14046  fsuppmapnn0fiub  14047  gsumval3lem1  20021  gsumval3lem2  20022  gsumval3  20023  gsumzres  20025  gsumzcl2  20026  gsumzf1o  20028  gsumzaddlem  20037  gsumconst  20050  gsumzoppg  20060  gsum2d  20088  dpjidcl  20176  gsumfsum  21636  regsumsupp  21824  frlmlbs  21999  psrass1lem  22135  psrass1  22165  psrass23l  22168  psrcom  22169  psrass23  22170  mplcoe1  22240  psropprmul  22449  coe1mul2  22482  tsmsgsum  24349  rrxcph  25604  rrxsuppss  25615  rrxmval  25617  mdegfval  26272  mdegleb  26274  mdegldg  26276  deg1mul3le  26327  wilthlem3  27287  suppovss  33099  fressupp  33106  ressupprn  33108  supppreima  33109  fsupprnfi  33110  fsuppcurry1  33141  fsuppcurry2  33142  gsumfs2d  33447  gsumhashmul  33453  elrgspnlem4  33631  elrgspnsubrunlem1  33633  elrgspnsubrunlem2  33634  elrspunidl  33802  rprmdvdsprod  33890  1arithidom  33893  esplymhp  34024  esplyfv1  34025  esplyfval3  34028  esplyfval1  34029  esplyfvaln  34030  esplyind  34031  fedgmullem1  34085  fldextrspunlsplem  34129  fldextrspunlsp  34130  zarcmplem  34337  fdivmpt  49379  fdivmptf  49380  refdivmptf  49381  fdivpm  49382  refdivpm  49383