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 ( 𝜑𝐷𝐴 )