Theorem ffdmd 6523

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3859  dom cdm 5525  ⟶wf 6332

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 3412  df-in 3866  df-ss 3876  df-fn 6339  df-f 6340

This theorem is referenced by:  ordtypelem5  9012  ablfaclem2  19269  ablfac2  19272  f1lindf  20580  lmcnp  21997  upgr1e  26998  upgrres1  27195  umgrres1  27196  umgr2v2e  27407  pliguhgr  28361  s3f1  30738  ccatf1  30740  swrdf1  30745  tocyccntz  30930  dfac21  40376  xlimmnfvlem1  42833  xlimpnfvlem1  42837  itgperiod  42982  issmfd  43728  issmfdf  43730  cnfsmf  43733  issmfled  43750  issmfgtd  43753  smfsuplem1  43801