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

Metamath Proof Explorer

Theorem fvresd

Description: The value of a restricted function, deduction version of fvres . (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypothesis fvresd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion fvresd ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fvresd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2 fvres ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
3 1 2 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )