Theorem ffdmd

Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	ffdmd.1	|- ( ph -> F : A --> B )
Assertion	ffdmd	|- ( ph -> F : dom F --> B )

Proof

Step	Hyp	Ref	Expression
1		ffdmd.1	|- ( ph -> F : A --> B )
2		ffdm	|- ( F : A --> B -> ( F : dom F --> B /\ dom F C_ A ) )
3	1 2	syl	|- ( ph -> ( F : dom F --> B /\ dom F C_ A ) )
4	3	simpld	|- ( ph -> F : dom F --> B )