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 3965	1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3890  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-fn 6495  df-f 6496

This theorem is referenced by:  fisuppfi  9277  wemapso  9459  wemapso2lem  9460  cantnfcl  9579  cantnfle  9583  cantnflt  9584  cantnff  9586  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1  9601  cantnflem3  9603  cnfcomlem  9611  cnfcom  9612  cnfcom3lem  9615  cnfcom3  9616  fin1a2lem7  10319  isercolllem2  15619  isercolllem3  15620  fsumss  15678  fprodss  15904  vdwlem1  16943  vdwlem5  16947  vdwlem6  16948  ghmpreima  19204  pmtrfconj  19432  gsumval3lem1  19871  gsumval3lem2  19872  gsumval3  19873  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzmhm  19903  gsumzoppg  19910  gsum2d  19938  dpjidcl  20026  lmhmpreima  21035  rhmpreimaidl  21267  gsumfsum  21424  regsumsupp  21612  frlmlbs  21787  mplcoe1  22025  mplcoe5  22028  psr1baslem  22158  mdetdiaglem  22573  cnclima  23243  iscncl  23244  cnclsi  23247  txcnmpt  23599  qtopval2  23671  qtopcn  23689  rnelfmlem  23927  fmfnfmlem4  23932  clssubg  24084  tgphaus  24092  tsmsgsum  24114  xmeter  24408  metustss  24526  metustexhalf  24531  restmetu  24545  rrxcph  25369  rrxsuppss  25380  mdegfval  26037  mdegleb  26039  mdegldg  26041  deg1mul3le  26092  plyeq0lem  26185  dgrcl  26208  dgrub  26209  dgrlb  26211  vieta1lem1  26287  suppovss  32769  pwrssmgc  33075  gsumfs2d  33137  gsumhashmul  33143  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrspunidl  33503  rprmdvdsprod  33609  1arithidom  33612  esplyfv1  33728  esplysply  33730  esplyfval3  33731  esplyfvaln  33733  dimkerim  33787  fedgmullem1  33789  lvecendof1f1o  33793  fldextrspunlsplem  33833  carsggect  34478  sibfof  34500  eulerpartlemsv2  34518  eulerpartlemsf  34519  eulerpartlemt  34531  eulerpartlemgu  34537  eulerpartlemgs2  34540  cvmliftmolem1  35479  cvmlift3lem6  35522  itg2addnclem  38006  keridl  38367  ismrcd1  43144  istopclsd  43146  pwfi2f1o  43542  sge0f1o  46828  smfsuplem1  47257