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

Proof

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