Metamath Proof Explorer


Theorem fdmi

Description: Inference associated with fdm . The domain of a mapping. (Contributed by NM, 28-Jul-2008)

Ref Expression
Hypothesis fdmi.1 F : A B
Assertion fdmi dom F = A

Proof

Step Hyp Ref Expression
1 fdmi.1 F : A B
2 fdm F : A B dom F = A
3 1 2 ax-mp dom F = A