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

Metamath Proof Explorer

Theorem funfnd

Description: A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis funfnd.1 ⊢ φ → Fun ⁡ A
Assertion funfnd ⊢ φ → A Fn dom ⁡ A

Proof

Step Hyp Ref Expression
1 funfnd.1 ⊢ φ → Fun ⁡ A
2 funfn ⊢ Fun ⁡ A ↔ A Fn dom ⁡ A
3 1 2 sylib ⊢ φ → A Fn dom ⁡ A