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


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