Theorem fssdm

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

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

Proof

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