Theorem suppssdm 8205

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 8189	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 4007	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	eqsstrdi 3956	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 8190	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4352	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	eqsstrdi 3956	. 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 2958  {crab 3415  Vcvv 3453   ⊆ wss 3899  ∅c0 4280  {csn 4587  dom cdm 5654   “ cima 5657  (class class class)co 7427   supp csupp 8187

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-sbc 3742  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-supp 8188

This theorem is used by:  snopsuppss  8207  wemapso2lem  9556  cantnfcl  9678  cantnfle  9682  cantnflt  9683  cantnff  9685  cantnfres  9688  cantnfp1lem3  9691  cantnflem1b  9697  cantnflem1  9700  cantnflem3  9702  cnfcomlem  9710  cnfcom  9711  cnfcom3lem  9714  cnfcom3  9715  fsuppmapnn0fiublem  14143  fsuppmapnn0fiub  14144  gsumval3lem1  20131  gsumval3lem2  20132  gsumval3  20133  gsumzres  20135  gsumzcl2  20136  gsumzf1o  20138  gsumzaddlem  20147  gsumconst  20160  gsumzoppg  20170  gsum2d  20198  dpjidcl  20286  gsumfsum  21752  regsumsupp  21940  frlmlbs  22115  psrass1lem  22253  psrass1  22283  psrass23l  22286  psrcom  22287  psrass23  22288  mplcoe1  22358  psropprmul  22567  coe1mul2  22600  tsmsgsum  24470  rrxcph  25725  rrxsuppss  25736  rrxmval  25738  mdegfval  26392  mdegleb  26394  mdegldg  26396  deg1mul3le  26447  wilthlem3  27409  suppovss  33328  fressupp  33335  ressupprn  33337  supppreima  33338  fsupprnfi  33339  fsuppcurry1  33369  fsuppcurry2  33370  gsumfs2d  33675  gsumhashmul  33681  elrgspnlem4  33859  elrgspnsubrunlem1  33861  elrgspnsubrunlem2  33862  elrspunidl  34031  rprmdvdsprod  34119  1arithidom  34122  esplymhp  34253  esplyfv1  34254  esplyfval3  34257  esplyfval1  34258  esplyfvaln  34259  esplyind  34260  fedgmullem1  34314  fldextrspunlsplem  34358  fldextrspunlsp  34359  zarcmplem  34566  fdivmpt  49791  fdivmptf  49792  refdivmptf  49793  fdivpm  49794  refdivpm  49795