Theorem ffdmd 6686

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3905  dom cdm 5623  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922  df-fn 6489  df-f 6490

This theorem is referenced by:  ordtypelem5  9433  ablfaclem2  19985  ablfac2  19988  f1lindf  21747  lmcnp  23207  upgr1e  29076  upgrres1  29276  umgrres1  29277  umgr2v2e  29489  pliguhgr  30448  s3f1  32901  ccatf1  32903  swrdf1  32911  tocyccntz  33099  dfac21  43039  xlimmnfvlem1  45814  xlimpnfvlem1  45818  itgperiod  45963  issmfd  46717  issmfdf  46719  cnfsmf  46722  issmfled  46739  issmfgtd  46743  smfsuplem1  46793  upgrimwlklem2  47883  upgrimtrlslem1  47889  upgrimtrlslem2  47890