Theorem ffdmd 6733

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 6732	. . 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 3899  dom cdm 5655  ⟶wf 6529

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916  df-fn 6536  df-f 6537

This theorem is used by:  ordtypelem5  9494  ccatf1  14656  swrdf1  14719  ablfaclem2  20215  ablfac2  20218  f1lindf  22035  lmcnp  23529  upgr1e  29570  upgrres1  29773  umgrres1  29774  umgr2v2e  29985  pliguhgr  30967  s3f1  33390  tocyccntz  33584  dfac21  43907  xlimmnfvlem1  46660  xlimpnfvlem1  46664  itgperiod  46809  fourierdlem48  46982  fourierdlem49  46983  fourierdlem113  47047  issmfd  47563  issmfdf  47565  cnfsmf  47568  issmfled  47585  issmfgtd  47589  smfsuplem1  47639  upgrimwlklem2  48814  upgrimtrlslem1  48820  upgrimtrlslem2  48821