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

Metamath Proof Explorer

Theorem ffdmd

Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis ffdmd.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion ffdmd ( 𝜑 → 𝐹 : dom 𝐹 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 ffdmd.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 ffdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) )
3 1 2 syl ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) )
4 3 simpld ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ 𝐵 )