Theorem ffdmd 6700

Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
ffdmd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffdmd	⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵)

Proof of Theorem ffdmd

Step	Hyp	Ref	Expression
1		ffdmd.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffdm 6699	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3903  dom cdm 5632  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-fn 6503  df-f 6504

This theorem is referenced by:  ordtypelem5  9439  ablfaclem2  20029  ablfac2  20032  f1lindf  21789  lmcnp  23260  upgr1e  29198  upgrres1  29398  umgrres1  29399  umgr2v2e  29611  pliguhgr  30573  s3f1  33039  ccatf1  33041  swrdf1  33048  tocyccntz  33237  dfac21  43420  xlimmnfvlem1  46187  xlimpnfvlem1  46191  itgperiod  46336  issmfd  47090  issmfdf  47092  cnfsmf  47095  issmfled  47112  issmfgtd  47116  smfsuplem1  47166  upgrimwlklem2  48255  upgrimtrlslem1  48261  upgrimtrlslem2  48262