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