Theorem suppssdm 8176

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 8161	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 4028	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3975	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 8162	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4350	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	eqsstrdi 3975	. 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 2145   ≠ wne 2955  {crab 3412  Vcvv 3450   ⊆ wss 3899  ∅c0 4279  {csn 4584  dom cdm 5655   “ cima 5658  (class class class)co 7414   supp csupp 8159

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-supp 8160

This theorem is used by:  snopsuppss  8178  wemapso2lem  9525  cantnfcl  9647  cantnfle  9651  cantnflt  9652  cantnff  9654  cantnfres  9657  cantnfp1lem3  9660  cantnflem1b  9666  cantnflem1  9669  cantnflem3  9671  cnfcomlem  9679  cnfcom  9680  cnfcom3lem  9683  cnfcom3  9684  fsuppmapnn0fiublem  14055  fsuppmapnn0fiub  14056  gsumval3lem1  20033  gsumval3lem2  20034  gsumval3  20035  gsumzres  20037  gsumzcl2  20038  gsumzf1o  20040  gsumzaddlem  20049  gsumconst  20062  gsumzoppg  20072  gsum2d  20100  dpjidcl  20188  gsumfsum  21648  regsumsupp  21836  frlmlbs  22011  psrass1lem  22149  psrass1  22179  psrass23l  22182  psrcom  22183  psrass23  22184  mplcoe1  22254  psropprmul  22463  coe1mul2  22496  tsmsgsum  24366  rrxcph  25621  rrxsuppss  25632  rrxmval  25634  mdegfval  26288  mdegleb  26290  mdegldg  26292  deg1mul3le  26343  wilthlem3  27307  suppovss  33154  fressupp  33161  ressupprn  33163  supppreima  33164  fsupprnfi  33165  fsuppcurry1  33196  fsuppcurry2  33197  gsumfs2d  33502  gsumhashmul  33508  elrgspnlem4  33686  elrgspnsubrunlem1  33688  elrgspnsubrunlem2  33689  elrspunidl  33857  rprmdvdsprod  33945  1arithidom  33948  esplymhp  34079  esplyfv1  34080  esplyfval3  34083  esplyfval1  34084  esplyfvaln  34085  esplyind  34086  fedgmullem1  34140  fldextrspunlsplem  34184  fldextrspunlsp  34185  zarcmplem  34392  fdivmpt  49471  fdivmptf  49472  refdivmptf  49473  fdivpm  49474  refdivpm  49475