Theorem fssdm 6755

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

Syntax hints:   → wi 4   ⊆ wss 3962  dom cdm 5688  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979  df-fn 6565  df-f 6566

This theorem is referenced by:  fisuppfi  9408  wemapso  9588  wemapso2lem  9589  cantnfcl  9704  cantnfle  9708  cantnflt  9709  cantnff  9711  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1  9726  cantnflem3  9728  cnfcomlem  9736  cnfcom  9737  cnfcom3lem  9740  cnfcom3  9741  fin1a2lem7  10443  isercolllem2  15698  isercolllem3  15699  fsumss  15757  fprodss  15980  vdwlem1  17014  vdwlem5  17018  vdwlem6  17019  ghmpreima  19268  pmtrfconj  19498  gsumval3lem1  19937  gsumval3lem2  19938  gsumval3  19939  gsumzres  19941  gsumzcl2  19942  gsumzf1o  19944  gsumzmhm  19969  gsumzoppg  19976  gsum2d  20004  dpjidcl  20092  lmhmpreima  21064  rhmpreimaidl  21304  gsumfsum  21469  regsumsupp  21657  frlmlbs  21834  mplcoe1  22072  mplcoe5  22075  psr1baslem  22201  mdetdiaglem  22619  cnclima  23291  iscncl  23292  cnclsi  23295  txcnmpt  23647  qtopval2  23719  qtopcn  23737  rnelfmlem  23975  fmfnfmlem4  23980  clssubg  24132  tgphaus  24140  tsmsgsum  24162  xmeter  24458  metustss  24579  metustexhalf  24584  restmetu  24598  rrxcph  25439  rrxsuppss  25450  mdegfval  26115  mdegleb  26117  mdegldg  26119  deg1mul3le  26170  plyeq0lem  26263  dgrcl  26286  dgrub  26287  dgrlb  26289  vieta1lem1  26366  suppovss  32695  pwrssmgc  32974  gsumfs2d  33040  gsumhashmul  33046  elrgspnlem4  33234  elrspunidl  33435  rprmdvdsprod  33541  1arithidom  33544  dimkerim  33654  fedgmullem1  33656  lvecendof1f1o  33660  carsggect  34299  sibfof  34321  eulerpartlemsv2  34339  eulerpartlemsf  34340  eulerpartlemt  34352  eulerpartlemgu  34358  eulerpartlemgs2  34361  cvmliftmolem1  35265  cvmlift3lem6  35308  itg2addnclem  37657  keridl  38018  ismrcd1  42685  istopclsd  42687  pwfi2f1o  43084  sge0f1o  46337  smfsuplem1  46766