Theorem fssdm 6354

Description: Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, semi-deduction form. (Contributed by AV, 21-Aug-2022.)

Hypotheses

Ref	Expression
fssdm.d	⊢ 𝐷 ⊆ dom 𝐹
fssdm.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
fssdm	⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Proof of Theorem fssdm

Step	Hyp	Ref	Expression
1		fssdm.d	. 2 ⊢ 𝐷 ⊆ dom 𝐹
2		fssdm.f	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6347	. 2 ⊢ (𝜑 → dom 𝐹 = 𝐴)
4	1, 3	syl5sseq 3905	1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3825  dom cdm 5400  ⟶wf 6178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-in 3832  df-ss 3839  df-fn 6185  df-f 6186

This theorem is referenced by:  fisuppfi  8628  wemapso  8802  wemapso2lem  8803  cantnfcl  8916  cantnfle  8920  cantnflt  8921  cantnff  8923  cantnfp1lem3  8929  cantnflem1b  8935  cantnflem1  8938  cantnflem3  8940  cnfcomlem  8948  cnfcom  8949  cnfcom3lem  8952  cnfcom3  8953  fin1a2lem7  9618  isercolllem2  14873  isercolllem3  14874  fsumss  14932  fprodss  15152  vdwlem1  16163  vdwlem5  16167  vdwlem6  16168  ghmpreima  18141  pmtrfconj  18345  gsumval3lem1  18769  gsumval3lem2  18770  gsumval3  18771  gsumzres  18773  gsumzcl2  18774  gsumzf1o  18776  gsumzmhm  18800  gsumzoppg  18807  gsum2d  18835  dpjidcl  18920  lmhmpreima  19532  mplcoe1  19949  mplcoe5  19952  psr1baslem  20046  gsumfsum  20304  regsumsupp  20458  frlmlbs  20633  mdetdiaglem  20901  cnclima  21570  iscncl  21571  cnclsi  21574  txcnmpt  21926  qtopval2  21998  qtopcn  22016  rnelfmlem  22254  fmfnfmlem4  22259  clssubg  22410  tgphaus  22418  tsmsgsum  22440  xmeter  22736  metustss  22854  metustexhalf  22859  restmetu  22873  rrxcph  23688  rrxsuppss  23699  mdegfval  24349  mdegleb  24351  mdegldg  24353  deg1mul3le  24403  plyeq0lem  24493  dgrcl  24516  dgrub  24517  dgrlb  24519  vieta1lem1  24592  suppovss  30176  dimkerim  30608  fedgmullem1  30610  carsggect  31178  sibfof  31200  eulerpartlemsv2  31218  eulerpartlemsf  31219  eulerpartlemt  31231  eulerpartlemgu  31237  eulerpartlemgs2  31240  cvmliftmolem1  32073  cvmlift3lem6  32116  itg2addnclem  34332  keridl  34700  ismrcd1  38635  istopclsd  38637  pwfi2f1o  39037  sge0f1o  42041  smfsuplem1  42462