Theorem ffdmd 6692

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3901  dom cdm 5624  ⟶wf 6488

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-fn 6495  df-f 6496

This theorem is referenced by:  ordtypelem5  9427  ablfaclem2  20017  ablfac2  20020  f1lindf  21777  lmcnp  23248  upgr1e  29186  upgrres1  29386  umgrres1  29387  umgr2v2e  29599  pliguhgr  30561  s3f1  33029  ccatf1  33031  swrdf1  33038  tocyccntz  33226  dfac21  43308  xlimmnfvlem1  46076  xlimpnfvlem1  46080  itgperiod  46225  issmfd  46979  issmfdf  46981  cnfsmf  46984  issmfled  47001  issmfgtd  47005  smfsuplem1  47055  upgrimwlklem2  48144  upgrimtrlslem1  48150  upgrimtrlslem2  48151