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

Metamath Proof Explorer

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

Proof

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