Theorem ffdmd 6717

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

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3902  dom cdm 5643  ⟶wf 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919  df-fn 6519  df-f 6520

This theorem is referenced by:  ordtypelem5  9464  ablfaclem2  20119  ablfac2  20122  f1lindf  21862  lmcnp  23352  upgr1e  29271  upgrres1  29471  umgrres1  29472  umgr2v2e  29683  pliguhgr  30646  s3f1  33086  ccatf1  33088  swrdf1  33095  tocyccntz  33285  dfac21  43604  xlimmnfvlem1  46367  xlimpnfvlem1  46371  itgperiod  46516  fourierdlem48  46689  fourierdlem49  46690  fourierdlem113  46754  issmfd  47270  issmfdf  47272  cnfsmf  47275  issmfled  47292  issmfgtd  47296  smfsuplem1  47346  upgrimwlklem2  48481  upgrimtrlslem1  48487  upgrimtrlslem2  48488