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 3895  dom cdm 5650  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896  df-fn 6542  df-f 6543

This theorem is used by:  ordtypelem5  9520  ccatf1  14740  swrdf1  14804  ablfaclem2  20308  ablfac2  20311  f1lindf  22134  lmcnp  23628  upgr1e  29697  upgrres1  29900  umgrres1  29901  umgr2v2e  30112  pliguhgr  31094  s3f1  33558  tocyccntz  33752  dfac21  44162  xlimmnfvlem1  46936  xlimpnfvlem1  46940  itgperiod  47085  fourierdlem48  47258  fourierdlem49  47259  fourierdlem113  47323  issmfd  47839  issmfdf  47841  cnfsmf  47844  issmfled  47861  issmfgtd  47865  smfsuplem1  47915  upgrimwlklem2  49090  upgrimtrlslem1  49096  upgrimtrlslem2  49097