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 𝐴 )
Assertion funfnd ( 𝜑 → 𝐴 Fn dom 𝐴 )

Proof

Step Hyp Ref Expression
1 funfnd.1 ⊢ ( 𝜑 → Fun 𝐴 )
2 funfn ⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )
3 1 2 sylib ⊢ ( 𝜑 → 𝐴 Fn dom 𝐴 )