Theorem ffdmd 6692

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3890  dom cdm 5624  ⟶wf 6488

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 3907  df-fn 6495  df-f 6496

This theorem is referenced by:  ordtypelem5  9430  ablfaclem2  20054  ablfac2  20057  f1lindf  21812  lmcnp  23279  upgr1e  29196  upgrres1  29396  umgrres1  29397  umgr2v2e  29609  pliguhgr  30572  s3f1  33022  ccatf1  33024  swrdf1  33031  tocyccntz  33220  dfac21  43512  xlimmnfvlem1  46278  xlimpnfvlem1  46282  itgperiod  46427  issmfd  47181  issmfdf  47183  cnfsmf  47186  issmfled  47203  issmfgtd  47207  smfsuplem1  47257  upgrimwlklem2  48386  upgrimtrlslem1  48392  upgrimtrlslem2  48393