Theorem ffdmd 6734

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3913  dom cdm 5659  ⟶wf 6529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-fn 6536  df-f 6537

This theorem is referenced by:  ordtypelem5  9480  ablfaclem2  20154  ablfac2  20157  f1lindf  21937  lmcnp  23426  upgr1e  29400  upgrres1  29600  umgrres1  29601  umgr2v2e  29812  pliguhgr  30775  s3f1  33204  ccatf1  33206  swrdf1  33213  tocyccntz  33401  dfac21  43678  xlimmnfvlem1  46431  xlimpnfvlem1  46435  itgperiod  46580  fourierdlem48  46753  fourierdlem49  46754  fourierdlem113  46818  issmfd  47334  issmfdf  47336  cnfsmf  47339  issmfled  47356  issmfgtd  47360  smfsuplem1  47410  upgrimwlklem2  48545  upgrimtrlslem1  48551  upgrimtrlslem2  48552