Metamath Proof Explorer

Theorem fdmd

Description: Deduction form of fdm . The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 fdmd.1 
 |-  ( ph -> F : A --> B )
2 fdm 
 |-  ( F : A --> B -> dom F = A )
3 1 2 syl 
 |-  ( ph -> dom F = A )