This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ffdmd

Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis ffdmd.1 
|- ( ph -> F : A --> B )
Assertion ffdmd 
|- ( ph -> F : dom F --> B )

Proof

Step Hyp Ref Expression
1 ffdmd.1 
 |-  ( ph -> F : A --> B )
2 ffdm 
 |-  ( F : A --> B -> ( F : dom F --> B /\ dom F C_ A ) )
3 1 2 syl 
 |-  ( ph -> ( F : dom F --> B /\ dom F C_ A ) )
4 3 simpld 
 |-  ( ph -> F : dom F --> B )