Theorem ffdmd 6692

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3890  dom cdm 5625  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907  df-fn 6495  df-f 6496

This theorem is referenced by:  ordtypelem5  9434  ablfaclem2  20061  ablfac2  20064  f1lindf  21804  lmcnp  23294  upgr1e  29207  upgrres1  29407  umgrres1  29408  umgr2v2e  29619  pliguhgr  30582  s3f1  33033  ccatf1  33035  swrdf1  33042  tocyccntz  33232  dfac21  43518  xlimmnfvlem1  46282  xlimpnfvlem1  46286  itgperiod  46431  issmfd  47185  issmfdf  47187  cnfsmf  47190  issmfled  47207  issmfgtd  47211  smfsuplem1  47261  upgrimwlklem2  48396  upgrimtrlslem1  48402  upgrimtrlslem2  48403