This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to F : A ⟶ B$
	fssdmd.d	$⊢ φ \to D \subseteq dom F$
Assertion	fssdmd	$⊢ φ \to D \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		fssdmd.f	$⊢ φ \to F : A ⟶ B$
2		fssdmd.d	$⊢ φ \to D \subseteq dom F$
3	1	fdmd	$⊢ φ \to dom F = A$
4	2 3	sseqtrd	$⊢ φ \to D \subseteq A$