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

Proof

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