Theorem ffdmd 6778

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3976  dom cdm 5700  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-fn 6576  df-f 6577

This theorem is referenced by:  ordtypelem5  9591  ablfaclem2  20130  ablfac2  20133  f1lindf  21865  lmcnp  23333  upgr1e  29148  upgrres1  29348  umgrres1  29349  umgr2v2e  29561  pliguhgr  30518  s3f1  32913  ccatf1  32915  swrdf1  32923  tocyccntz  33137  dfac21  43023  xlimmnfvlem1  45753  xlimpnfvlem1  45757  itgperiod  45902  issmfd  46656  issmfdf  46658  cnfsmf  46661  issmfled  46678  issmfgtd  46682  smfsuplem1  46732