Metamath Proof Explorer

Theorem fveqres

Description: Equal values imply equal values in a restriction. (Contributed by NM, 13-Nov-1995)

Ref Expression
Assertion fveqres ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fvres ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
2 fvres ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
3 1 2 eqeq12d ⊢ ( 𝐴 ∈ 𝐵 → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) ↔ ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) )
4 3 biimprd ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) ) )
5 nfvres ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ )
6 nfvres ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ )
7 5 6 eqtr4d ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) )
8 7 a1d ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) ) )
9 4 8 pm2.61i ⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝐴 ) )