Metamath Proof Explorer

Theorem fdm

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion fdm F : A B dom F = A


Step Hyp Ref Expression
1 ffn F : A B F Fn A
2 fndm F Fn A dom F = A
3 1 2 syl F : A B dom F = A