Theorem suppssdm 7353

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 7342	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2		ssrab2 3720	. . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
3	1, 2	syl6eqss 3688	. 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4		supp0prc 7343	. . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5		0ss 4005	. . 3 ⊢ ∅ ⊆ dom 𝐹
6	4, 5	syl6eqss 3688	. 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
7	3, 6	pm2.61i 176	1 ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹

Syntax hints:  ¬ wn 3   ∧ wa 383   ∈ wcel 2030   ≠ wne 2823  {crab 2945  Vcvv 3231   ⊆ wss 3607  ∅c0 3948  {csn 4210  dom cdm 5143   “ cima 5146  (class class class)co 6690   supp csupp 7340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-supp 7341

This theorem is referenced by:  snopsuppss  7355  wemapso2lem  8498  cantnfcl  8602  cantnfle  8606  cantnflt  8607  cantnff  8609  cantnfres  8612  cantnfp1lem2  8614  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1d  8623  cantnflem1  8624  cantnflem3  8626  cnfcomlem  8634  cnfcom  8635  cnfcom2lem  8636  cnfcom3lem  8638  cnfcom3  8639  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzoppg  18390  gsum2d  18417  dpjidcl  18503  psrass1lem  19425  psrass1  19453  psrass23l  19456  psrcom  19457  psrass23  19458  mplcoe1  19513  psropprmul  19656  coe1mul2  19687  gsumfsum  19861  regsumsupp  20016  frlmlbs  20184  tsmsgsum  21989  rrxcph  23226  rrxsuppss  23232  rrxmval  23234  mdegfval  23867  mdegleb  23869  mdegldg  23871  deg1mul3le  23921  wilthlem3  24841  fdivmpt  42659  fdivmptf  42660  refdivmptf  42661  fdivpm  42662  refdivpm  42663