Theorem ffdmd 6741

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3914  dom cdm 5651  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3915  df-fn 6542  df-f 6543

This theorem is used by:  ordtypelem5  9517  ccatf1  14737  swrdf1  14800  ablfaclem2  20303  ablfac2  20306  f1lindf  22129  lmcnp  23623  upgr1e  29692  upgrres1  29895  umgrres1  29896  umgr2v2e  30107  pliguhgr  31089  s3f1  33512  tocyccntz  33706  dfac21  44069  xlimmnfvlem1  46843  xlimpnfvlem1  46847  itgperiod  46992  fourierdlem48  47165  fourierdlem49  47166  fourierdlem113  47230  issmfd  47746  issmfdf  47748  cnfsmf  47751  issmfled  47768  issmfgtd  47772  smfsuplem1  47822  upgrimwlklem2  48997  upgrimtrlslem1  49003  upgrimtrlslem2  49004