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

Syntax hints:   → wi 4   ⊆ wss 3951  dom cdm 5685  ⟶wf 6557

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-fn 6564  df-f 6565

This theorem is referenced by:  fisuppfi  9411  wemapso  9591  wemapso2lem  9592  cantnfcl  9707  cantnfle  9711  cantnflt  9712  cantnff  9714  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  cantnflem3  9731  cnfcomlem  9739  cnfcom  9740  cnfcom3lem  9743  cnfcom3  9744  fin1a2lem7  10446  isercolllem2  15702  isercolllem3  15703  fsumss  15761  fprodss  15984  vdwlem1  17019  vdwlem5  17023  vdwlem6  17024  ghmpreima  19256  pmtrfconj  19484  gsumval3lem1  19923  gsumval3lem2  19924  gsumval3  19925  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzmhm  19955  gsumzoppg  19962  gsum2d  19990  dpjidcl  20078  lmhmpreima  21047  rhmpreimaidl  21287  gsumfsum  21452  regsumsupp  21640  frlmlbs  21817  mplcoe1  22055  mplcoe5  22058  psr1baslem  22186  mdetdiaglem  22604  cnclima  23276  iscncl  23277  cnclsi  23280  txcnmpt  23632  qtopval2  23704  qtopcn  23722  rnelfmlem  23960  fmfnfmlem4  23965  clssubg  24117  tgphaus  24125  tsmsgsum  24147  xmeter  24443  metustss  24564  metustexhalf  24569  restmetu  24583  rrxcph  25426  rrxsuppss  25437  mdegfval  26101  mdegleb  26103  mdegldg  26105  deg1mul3le  26156  plyeq0lem  26249  dgrcl  26272  dgrub  26273  dgrlb  26275  vieta1lem1  26352  suppovss  32690  pwrssmgc  32990  gsumfs2d  33058  gsumhashmul  33064  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrspunidl  33456  rprmdvdsprod  33562  1arithidom  33565  dimkerim  33678  fedgmullem1  33680  lvecendof1f1o  33684  fldextrspunlsplem  33723  carsggect  34320  sibfof  34342  eulerpartlemsv2  34360  eulerpartlemsf  34361  eulerpartlemt  34373  eulerpartlemgu  34379  eulerpartlemgs2  34382  cvmliftmolem1  35286  cvmlift3lem6  35329  itg2addnclem  37678  keridl  38039  ismrcd1  42709  istopclsd  42711  pwfi2f1o  43108  sge0f1o  46397  smfsuplem1  46826