Theorem fssdm 6620

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

Syntax hints:   → wi 4   ⊆ wss 3887  dom cdm 5589  ⟶wf 6429

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-fn 6436  df-f 6437

This theorem is referenced by:  fisuppfi  9136  wemapso  9310  wemapso2lem  9311  cantnfcl  9425  cantnfle  9429  cantnflt  9430  cantnff  9432  cantnfp1lem3  9438  cantnflem1b  9444  cantnflem1  9447  cantnflem3  9449  cnfcomlem  9457  cnfcom  9458  cnfcom3lem  9461  cnfcom3  9462  fin1a2lem7  10162  isercolllem2  15377  isercolllem3  15378  fsumss  15437  fprodss  15658  vdwlem1  16682  vdwlem5  16686  vdwlem6  16687  ghmpreima  18856  pmtrfconj  19074  gsumval3lem1  19506  gsumval3lem2  19507  gsumval3  19508  gsumzres  19510  gsumzcl2  19511  gsumzf1o  19513  gsumzmhm  19538  gsumzoppg  19545  gsum2d  19573  dpjidcl  19661  lmhmpreima  20310  gsumfsum  20665  regsumsupp  20827  frlmlbs  21004  mplcoe1  21238  mplcoe5  21241  psr1baslem  21356  mdetdiaglem  21747  cnclima  22419  iscncl  22420  cnclsi  22423  txcnmpt  22775  qtopval2  22847  qtopcn  22865  rnelfmlem  23103  fmfnfmlem4  23108  clssubg  23260  tgphaus  23268  tsmsgsum  23290  xmeter  23586  metustss  23707  metustexhalf  23712  restmetu  23726  rrxcph  24556  rrxsuppss  24567  mdegfval  25227  mdegleb  25229  mdegldg  25231  deg1mul3le  25281  plyeq0lem  25371  dgrcl  25394  dgrub  25395  dgrlb  25397  vieta1lem1  25470  suppovss  31017  pwrssmgc  31278  gsumhashmul  31316  rhmpreimaidl  31603  elrspunidl  31606  dimkerim  31708  fedgmullem1  31710  carsggect  32285  sibfof  32307  eulerpartlemsv2  32325  eulerpartlemsf  32326  eulerpartlemt  32338  eulerpartlemgu  32344  eulerpartlemgs2  32347  cvmliftmolem1  33243  cvmlift3lem6  33286  itg2addnclem  35828  keridl  36190  ismrcd1  40520  istopclsd  40522  pwfi2f1o  40921  sge0f1o  43920  smfsuplem1  44344