Theorem ffdmd 6738

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 6737	. . 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 5651  ⟶wf 6533

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 3916  df-fn 6540  df-f 6541

This theorem is used by:  ordtypelem5  9509  ccatf1  14729  swrdf1  14792  ablfaclem2  20295  ablfac2  20298  f1lindf  22121  lmcnp  23615  upgr1e  29684  upgrres1  29887  umgrres1  29888  umgr2v2e  30099  pliguhgr  31081  s3f1  33504  tocyccntz  33698  dfac21  44052  xlimmnfvlem1  46811  xlimpnfvlem1  46815  itgperiod  46960  fourierdlem48  47133  fourierdlem49  47134  fourierdlem113  47198  issmfd  47714  issmfdf  47716  cnfsmf  47719  issmfled  47736  issmfgtd  47740  smfsuplem1  47790  upgrimwlklem2  48965  upgrimtrlslem1  48971  upgrimtrlslem2  48972