Theorem fssdm 6724

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

Syntax hints:   → wi 4   ⊆ wss 3926  dom cdm 5654  ⟶wf 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-fn 6533  df-f 6534

This theorem is referenced by:  fisuppfi  9381  wemapso  9563  wemapso2lem  9564  cantnfcl  9679  cantnfle  9683  cantnflt  9684  cantnff  9686  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1  9701  cantnflem3  9703  cnfcomlem  9711  cnfcom  9712  cnfcom3lem  9715  cnfcom3  9716  fin1a2lem7  10418  isercolllem2  15680  isercolllem3  15681  fsumss  15739  fprodss  15962  vdwlem1  16999  vdwlem5  17003  vdwlem6  17004  ghmpreima  19219  pmtrfconj  19445  gsumval3lem1  19884  gsumval3lem2  19885  gsumval3  19886  gsumzres  19888  gsumzcl2  19889  gsumzf1o  19891  gsumzmhm  19916  gsumzoppg  19923  gsum2d  19951  dpjidcl  20039  lmhmpreima  21004  rhmpreimaidl  21236  gsumfsum  21400  regsumsupp  21580  frlmlbs  21755  mplcoe1  21993  mplcoe5  21996  psr1baslem  22118  mdetdiaglem  22534  cnclima  23204  iscncl  23205  cnclsi  23208  txcnmpt  23560  qtopval2  23632  qtopcn  23650  rnelfmlem  23888  fmfnfmlem4  23893  clssubg  24045  tgphaus  24053  tsmsgsum  24075  xmeter  24370  metustss  24488  metustexhalf  24493  restmetu  24507  rrxcph  25342  rrxsuppss  25353  mdegfval  26017  mdegleb  26019  mdegldg  26021  deg1mul3le  26072  plyeq0lem  26165  dgrcl  26188  dgrub  26189  dgrlb  26191  vieta1lem1  26268  suppovss  32604  pwrssmgc  32926  gsumfs2d  32995  gsumhashmul  33001  elrgspnlem4  33186  elrgspnsubrunlem1  33188  elrspunidl  33389  rprmdvdsprod  33495  1arithidom  33498  dimkerim  33613  fedgmullem1  33615  lvecendof1f1o  33619  fldextrspunlsplem  33660  carsggect  34296  sibfof  34318  eulerpartlemsv2  34336  eulerpartlemsf  34337  eulerpartlemt  34349  eulerpartlemgu  34355  eulerpartlemgs2  34358  cvmliftmolem1  35249  cvmlift3lem6  35292  itg2addnclem  37641  keridl  38002  ismrcd1  42668  istopclsd  42670  pwfi2f1o  43067  sge0f1o  46359  smfsuplem1  46788