Theorem fssdm 6738

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

Syntax hints:   → wi 4   ⊆ wss 3949  dom cdm 5677  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-fn 6547  df-f 6548

This theorem is referenced by:  fisuppfi  9370  wemapso  9546  wemapso2lem  9547  cantnfcl  9662  cantnfle  9666  cantnflt  9667  cantnff  9669  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1  9684  cantnflem3  9686  cnfcomlem  9694  cnfcom  9695  cnfcom3lem  9698  cnfcom3  9699  fin1a2lem7  10401  isercolllem2  15612  isercolllem3  15613  fsumss  15671  fprodss  15892  vdwlem1  16914  vdwlem5  16918  vdwlem6  16919  ghmpreima  19114  pmtrfconj  19334  gsumval3lem1  19773  gsumval3lem2  19774  gsumval3  19775  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzmhm  19805  gsumzoppg  19812  gsum2d  19840  dpjidcl  19928  lmhmpreima  20659  gsumfsum  21012  regsumsupp  21175  frlmlbs  21352  mplcoe1  21592  mplcoe5  21595  psr1baslem  21709  mdetdiaglem  22100  cnclima  22772  iscncl  22773  cnclsi  22776  txcnmpt  23128  qtopval2  23200  qtopcn  23218  rnelfmlem  23456  fmfnfmlem4  23461  clssubg  23613  tgphaus  23621  tsmsgsum  23643  xmeter  23939  metustss  24060  metustexhalf  24065  restmetu  24079  rrxcph  24909  rrxsuppss  24920  mdegfval  25580  mdegleb  25582  mdegldg  25584  deg1mul3le  25634  plyeq0lem  25724  dgrcl  25747  dgrub  25748  dgrlb  25750  vieta1lem1  25823  suppovss  31906  pwrssmgc  32170  gsumhashmul  32208  rhmpreimaidl  32537  elrspunidl  32546  dimkerim  32712  fedgmullem1  32714  carsggect  33317  sibfof  33339  eulerpartlemsv2  33357  eulerpartlemsf  33358  eulerpartlemt  33370  eulerpartlemgu  33376  eulerpartlemgs2  33379  cvmliftmolem1  34272  cvmlift3lem6  34315  itg2addnclem  36539  keridl  36900  ismrcd1  41436  istopclsd  41438  pwfi2f1o  41838  sge0f1o  45098  smfsuplem1  45527