Theorem ffdmd 6681

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3902  dom cdm 5616  ⟶wf 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919  df-fn 6484  df-f 6485

This theorem is referenced by:  ordtypelem5  9408  ablfaclem2  20001  ablfac2  20004  f1lindf  21760  lmcnp  23220  upgr1e  29092  upgrres1  29292  umgrres1  29293  umgr2v2e  29505  pliguhgr  30464  s3f1  32926  ccatf1  32928  swrdf1  32935  tocyccntz  33111  dfac21  43105  xlimmnfvlem1  45876  xlimpnfvlem1  45880  itgperiod  46025  issmfd  46779  issmfdf  46781  cnfsmf  46784  issmfled  46801  issmfgtd  46805  smfsuplem1  46855  upgrimwlklem2  47935  upgrimtrlslem1  47941  upgrimtrlslem2  47942