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 φ F : A B
fssdmd.d φ D dom F
Assertion fssdmd φ D A

Proof

Step Hyp Ref Expression
1 fssdmd.f φ F : A B
2 fssdmd.d φ D dom F
3 1 fdmd φ dom F = A
4 2 3 sseqtrd φ D A