Metamath Proof Explorer

Theorem fdm

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994) (Proof shortened by Wolf Lammen, 29-May-2024)

Ref Expression
Assertion fdm 
|- ( F : A --> B -> dom F = A )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 1 fndmd 
 |-  ( F : A --> B -> dom F = A )