Theorem ffdmd 6738

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3906  dom cdm 5663  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923  df-fn 6541  df-f 6542

This theorem is referenced by:  ordtypelem5  9485  ablfaclem2  20159  ablfac2  20162  f1lindf  21953  lmcnp  23442  upgr1e  29444  upgrres1  29644  umgrres1  29645  umgr2v2e  29856  pliguhgr  30819  s3f1  33248  ccatf1  33250  swrdf1  33257  tocyccntz  33445  dfac21  43776  xlimmnfvlem1  46529  xlimpnfvlem1  46533  itgperiod  46678  fourierdlem48  46851  fourierdlem49  46852  fourierdlem113  46916  issmfd  47432  issmfdf  47434  cnfsmf  47437  issmfled  47454  issmfgtd  47458  smfsuplem1  47508  upgrimwlklem2  48646  upgrimtrlslem1  48652  upgrimtrlslem2  48653