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

Metamath Proof Explorer

Theorem fveqres

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

Ref Expression
Assertion fveqres ⊢ F ⁡ A = G ⁡ A → F ↾ B ⁡ A = G ↾ B ⁡ A

Proof

Step Hyp Ref Expression
1 fvres ⊢ A ∈ B → F ↾ B ⁡ A = F ⁡ A
2 fvres ⊢ A ∈ B → G ↾ B ⁡ A = G ⁡ A
3 1 2 eqeq12d ⊢ A ∈ B → F ↾ B ⁡ A = G ↾ B ⁡ A ↔ F ⁡ A = G ⁡ A
4 3 biimprd ⊢ A ∈ B → F ⁡ A = G ⁡ A → F ↾ B ⁡ A = G ↾ B ⁡ A
5 nfvres ⊢ ¬ A ∈ B → F ↾ B ⁡ A = ∅
6 nfvres ⊢ ¬ A ∈ B → G ↾ B ⁡ A = ∅
7 5 6 eqtr4d ⊢ ¬ A ∈ B → F ↾ B ⁡ A = G ↾ B ⁡ A
8 7 a1d ⊢ ¬ A ∈ B → F ⁡ A = G ⁡ A → F ↾ B ⁡ A = G ↾ B ⁡ A
9 4 8 pm2.61i ⊢ F ⁡ A = G ⁡ A → F ↾ B ⁡ A = G ↾ B ⁡ A