Theorem ffdmd 6741

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3931  dom cdm 5659  ⟶wf 6532

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948  df-fn 6539  df-f 6540

This theorem is referenced by:  ordtypelem5  9541  ablfaclem2  20074  ablfac2  20077  f1lindf  21787  lmcnp  23247  upgr1e  29097  upgrres1  29297  umgrres1  29298  umgr2v2e  29510  pliguhgr  30472  s3f1  32927  ccatf1  32929  swrdf1  32937  tocyccntz  33160  dfac21  43057  xlimmnfvlem1  45828  xlimpnfvlem1  45832  itgperiod  45977  issmfd  46731  issmfdf  46733  cnfsmf  46736  issmfled  46753  issmfgtd  46757  smfsuplem1  46807  upgrimwlklem2  47878  upgrimtrlslem1  47884  upgrimtrlslem2  47885