Theorem ffdmd 6718

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3914  dom cdm 5638  ⟶wf 6507

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-fn 6514  df-f 6515

This theorem is referenced by:  ordtypelem5  9475  ablfaclem2  20018  ablfac2  20021  f1lindf  21731  lmcnp  23191  upgr1e  29040  upgrres1  29240  umgrres1  29241  umgr2v2e  29453  pliguhgr  30415  s3f1  32868  ccatf1  32870  swrdf1  32878  tocyccntz  33101  dfac21  43055  xlimmnfvlem1  45830  xlimpnfvlem1  45834  itgperiod  45979  issmfd  46733  issmfdf  46735  cnfsmf  46738  issmfled  46755  issmfgtd  46759  smfsuplem1  46809  upgrimwlklem2  47895  upgrimtrlslem1  47901  upgrimtrlslem2  47902