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

Syntax hints:   → wi 4   ⊆ wss 3890  dom cdm 5625  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907  df-fn 6495  df-f 6496

This theorem is referenced by:  fisuppfi  9281  wemapso  9463  wemapso2lem  9464  cantnfcl  9586  cantnfle  9590  cantnflt  9591  cantnff  9593  cantnfp1lem3  9599  cantnflem1b  9605  cantnflem1  9608  cantnflem3  9610  cnfcomlem  9618  cnfcom  9619  cnfcom3lem  9622  cnfcom3  9623  fin1a2lem7  10326  isercolllem2  15626  isercolllem3  15627  fsumss  15685  fprodss  15911  vdwlem1  16950  vdwlem5  16954  vdwlem6  16955  ghmpreima  19211  pmtrfconj  19439  gsumval3lem1  19878  gsumval3lem2  19879  gsumval3  19880  gsumzres  19882  gsumzcl2  19883  gsumzf1o  19885  gsumzmhm  19910  gsumzoppg  19917  gsum2d  19945  dpjidcl  20033  lmhmpreima  21045  rhmpreimaidl  21277  gsumfsum  21416  regsumsupp  21604  frlmlbs  21779  mplcoe1  22020  mplcoe5  22023  psr1baslem  22177  mdetdiaglem  22588  cnclima  23258  iscncl  23259  cnclsi  23262  txcnmpt  23614  qtopval2  23686  qtopcn  23704  rnelfmlem  23942  fmfnfmlem4  23947  clssubg  24099  tgphaus  24107  tsmsgsum  24129  xmeter  24423  metustss  24541  metustexhalf  24546  restmetu  24560  rrxcph  25384  rrxsuppss  25395  mdegfval  26052  mdegleb  26054  mdegldg  26056  deg1mul3le  26107  plyeq0lem  26200  dgrcl  26223  dgrub  26224  dgrlb  26226  vieta1lem1  26301  suppovss  32780  pwrssmgc  33086  gsumfs2d  33149  gsumhashmul  33155  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrspunidl  33518  rprmdvdsprod  33624  1arithidom  33627  esplyfv1  33760  esplysply  33762  esplyfval3  33763  esplyfvaln  33765  dimkerim  33818  fedgmullem1  33820  lvecendof1f1o  33824  fldextrspunlsplem  33864  carsggect  34509  sibfof  34531  eulerpartlemsv2  34549  eulerpartlemsf  34550  eulerpartlemt  34562  eulerpartlemgu  34568  eulerpartlemgs2  34571  cvmliftmolem1  35516  cvmlift3lem6  35559  itg2addnclem  38045  keridl  38406  ismrcd1  43154  istopclsd  43156  pwfi2f1o  43548  sge0f1o  46832  smfsuplem1  47261