Theorem ffdmd 6770

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 6769	. . 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 3900  dom cdm 5658  ⟶wf 6562

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-fn 6569  df-f 6570

This theorem is used by:  ordtypelem5  9553  ccatf1  14777  swrdf1  14841  ablfaclem2  20353  ablfac2  20356  f1lindf  22183  lmcnp  23677  upgr1e  29748  upgrres1  29951  umgrres1  29952  umgr2v2e  30163  pliguhgr  31145  s3f1  33607  tocyccntz  33804  dfac21  44334  xlimmnfvlem1  47115  xlimpnfvlem1  47119  itgperiod  47264  fourierdlem48  47437  fourierdlem49  47438  fourierdlem113  47502  issmfd  48018  issmfdf  48020  cnfsmf  48023  issmfled  48040  issmfgtd  48044  smfsuplem1  48094  upgrimwlklem2  49269  upgrimtrlslem1  49275  upgrimtrlslem2  49276