Theorem fssdmd

Description: Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, deduction form. (Contributed by AV, 21-Aug-2022)

	Ref	Expression
Hypotheses	fssdmd.f	|- ( ph -> F : A --> B )
	fssdmd.d	|- ( ph -> D C_ dom F )
Assertion	fssdmd	|- ( ph -> D C_ A )

Proof

Step	Hyp	Ref	Expression
1		fssdmd.f	|- ( ph -> F : A --> B )
2		fssdmd.d	|- ( ph -> D C_ dom F )
3	1	fdmd	|- ( ph -> dom F = A )
4	2 3	sseqtrd	|- ( ph -> D C_ A )