This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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