Theorem ffdmd 6765

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 6764	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3950  dom cdm 5684  ⟶wf 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ss 3967  df-fn 6563  df-f 6564

This theorem is referenced by:  ordtypelem5  9563  ablfaclem2  20107  ablfac2  20110  f1lindf  21843  lmcnp  23313  upgr1e  29131  upgrres1  29331  umgrres1  29332  umgr2v2e  29544  pliguhgr  30506  s3f1  32932  ccatf1  32934  swrdf1  32942  tocyccntz  33165  dfac21  43083  xlimmnfvlem1  45852  xlimpnfvlem1  45856  itgperiod  46001  issmfd  46755  issmfdf  46757  cnfsmf  46760  issmfled  46777  issmfgtd  46781  smfsuplem1  46831