Theorem ffdmd 6688

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3898  dom cdm 5621  ⟶wf 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915  df-fn 6491  df-f 6492

This theorem is referenced by:  ordtypelem5  9417  ablfaclem2  20004  ablfac2  20007  f1lindf  21763  lmcnp  23222  upgr1e  29095  upgrres1  29295  umgrres1  29296  umgr2v2e  29508  pliguhgr  30470  s3f1  32937  ccatf1  32939  swrdf1  32946  tocyccntz  33122  dfac21  43186  xlimmnfvlem1  45957  xlimpnfvlem1  45961  itgperiod  46106  issmfd  46860  issmfdf  46862  cnfsmf  46865  issmfled  46882  issmfgtd  46886  smfsuplem1  46936  upgrimwlklem2  48025  upgrimtrlslem1  48031  upgrimtrlslem2  48032