Theorem ffdmd 6698

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3889  dom cdm 5631  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-fn 6501  df-f 6502

This theorem is referenced by:  ordtypelem5  9437  ablfaclem2  20063  ablfac2  20066  f1lindf  21802  lmcnp  23269  upgr1e  29182  upgrres1  29382  umgrres1  29383  umgr2v2e  29594  pliguhgr  30557  s3f1  33007  ccatf1  33009  swrdf1  33016  tocyccntz  33205  dfac21  43494  xlimmnfvlem1  46260  xlimpnfvlem1  46264  itgperiod  46409  issmfd  47163  issmfdf  47165  cnfsmf  47168  issmfled  47185  issmfgtd  47189  smfsuplem1  47239  upgrimwlklem2  48374  upgrimtrlslem1  48380  upgrimtrlslem2  48381