Metamath Proof Explorer

Theorem fndmd

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

Ref Expression
Hypothesis fndmd.1 
|- ( ph -> F Fn A )
Assertion fndmd 
|- ( ph -> dom F = A )

Proof

Step Hyp Ref Expression
1 fndmd.1 
 |-  ( ph -> F Fn A )
2 fndm 
 |-  ( F Fn A -> dom F = A )
3 1 2 syl 
 |-  ( ph -> dom F = A )