Theorem ffdmd 6767

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3963  dom cdm 5689  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980  df-fn 6566  df-f 6567

This theorem is referenced by:  ordtypelem5  9560  ablfaclem2  20121  ablfac2  20124  f1lindf  21860  lmcnp  23328  upgr1e  29145  upgrres1  29345  umgrres1  29346  umgr2v2e  29558  pliguhgr  30515  s3f1  32916  ccatf1  32918  swrdf1  32926  tocyccntz  33147  dfac21  43055  xlimmnfvlem1  45788  xlimpnfvlem1  45792  itgperiod  45937  issmfd  46691  issmfdf  46693  cnfsmf  46696  issmfled  46713  issmfgtd  46717  smfsuplem1  46767