Theorem ffdmd 6515

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3854  dom cdm 5517  ⟶wf 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3409  df-in 3861  df-ss 3871  df-fn 6331  df-f 6332

This theorem is referenced by:  ordtypelem5  9004  ablfaclem2  19261  ablfac2  19264  f1lindf  20572  lmcnp  21989  upgr1e  26990  upgrres1  27187  umgrres1  27188  umgr2v2e  27399  pliguhgr  28353  s3f1  30730  ccatf1  30732  swrdf1  30737  tocyccntz  30922  dfac21  40368  xlimmnfvlem1  42825  xlimpnfvlem1  42829  itgperiod  42974  issmfd  43720  issmfdf  43722  cnfsmf  43725  issmfled  43742  issmfgtd  43745  smfsuplem1  43793