Theorem ffdmd 6740

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 6739	. . 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 3906  dom cdm 5663  ⟶wf 6536

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-fn 6543  df-f 6544

This theorem is used by:  ordtypelem5  9487  ccatf1  14641  swrdf1  14704  ablfaclem2  20181  ablfac2  20184  f1lindf  22001  lmcnp  23490  upgr1e  29492  upgrres1  29692  umgrres1  29693  umgr2v2e  29904  pliguhgr  30867  s3f1  33293  tocyccntz  33487  dfac21  43826  xlimmnfvlem1  46579  xlimpnfvlem1  46583  itgperiod  46728  fourierdlem48  46901  fourierdlem49  46902  fourierdlem113  46966  issmfd  47482  issmfdf  47484  cnfsmf  47487  issmfled  47504  issmfgtd  47508  smfsuplem1  47558  upgrimwlklem2  48696  upgrimtrlslem1  48702  upgrimtrlslem2  48703