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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fssdmd.d	⊢ ( 𝜑 → 𝐷 ⊆ dom 𝐹 )
Assertion	fssdmd	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fssdmd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fssdmd.d	⊢ ( 𝜑 → 𝐷 ⊆ dom 𝐹 )
3	1	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
4	2 3	sseqtrd	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )