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 
|- D C_ dom F
fssdm.f 
|- ( ph -> F : A --> B )
Assertion fssdm 
|- ( ph -> D C_ A )

Proof

Step Hyp Ref Expression
1 fssdm.d 
 |-  D C_ dom F
2 fssdm.f 
 |-  ( ph -> F : A --> B )
3 2 fdmd 
 |-  ( ph -> dom F = A )
4 1 3 sseqtrid 
 |-  ( ph -> D C_ A )