Theorem fssdm 6681

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 6672	. 2 ⊢ (𝜑 → dom 𝐹 = 𝐴)
4	1, 3	sseqtrid 3976	1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3901  dom cdm 5624  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-fn 6495  df-f 6496

This theorem is referenced by:  fisuppfi  9274  wemapso  9456  wemapso2lem  9457  cantnfcl  9576  cantnfle  9580  cantnflt  9581  cantnff  9583  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1  9598  cantnflem3  9600  cnfcomlem  9608  cnfcom  9609  cnfcom3lem  9612  cnfcom3  9613  fin1a2lem7  10316  isercolllem2  15589  isercolllem3  15590  fsumss  15648  fprodss  15871  vdwlem1  16909  vdwlem5  16913  vdwlem6  16914  ghmpreima  19167  pmtrfconj  19395  gsumval3lem1  19834  gsumval3lem2  19835  gsumval3  19836  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzmhm  19866  gsumzoppg  19873  gsum2d  19901  dpjidcl  19989  lmhmpreima  21000  rhmpreimaidl  21232  gsumfsum  21389  regsumsupp  21577  frlmlbs  21752  mplcoe1  21992  mplcoe5  21995  psr1baslem  22125  mdetdiaglem  22542  cnclima  23212  iscncl  23213  cnclsi  23216  txcnmpt  23568  qtopval2  23640  qtopcn  23658  rnelfmlem  23896  fmfnfmlem4  23901  clssubg  24053  tgphaus  24061  tsmsgsum  24083  xmeter  24377  metustss  24495  metustexhalf  24500  restmetu  24514  rrxcph  25348  rrxsuppss  25359  mdegfval  26023  mdegleb  26025  mdegldg  26027  deg1mul3le  26078  plyeq0lem  26171  dgrcl  26194  dgrub  26195  dgrlb  26197  vieta1lem1  26274  suppovss  32760  pwrssmgc  33082  gsumfs2d  33144  gsumhashmul  33150  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrspunidl  33509  rprmdvdsprod  33615  1arithidom  33618  esplyfv1  33727  esplysply  33729  esplyfval3  33730  dimkerim  33784  fedgmullem1  33786  lvecendof1f1o  33790  fldextrspunlsplem  33830  carsggect  34475  sibfof  34497  eulerpartlemsv2  34515  eulerpartlemsf  34516  eulerpartlemt  34528  eulerpartlemgu  34534  eulerpartlemgs2  34537  cvmliftmolem1  35475  cvmlift3lem6  35518  itg2addnclem  37872  keridl  38233  ismrcd1  42940  istopclsd  42942  pwfi2f1o  43338  sge0f1o  46626  smfsuplem1  47055