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

Metamath Proof Explorer

Theorem fdm

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994) (Proof shortened by Wolf Lammen, 29-May-2024)

Ref Expression
Assertion fdm ⊢ F : A ⟶ B → dom ⁡ F = A

Proof

Step Hyp Ref Expression
1 ffn ⊢ F : A ⟶ B → F Fn A
2 1 fndmd ⊢ F : A ⟶ B → dom ⁡ F = A