This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Equality of restricted functions is determined by their values.
(Contributed by NM, 3-Aug-1994) (Proof shortened by AV, 4-Mar-2019)
|
|
Ref |
Expression |
|
Assertion |
fvreseq |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fvreseq0 |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) |
| 2 |
1
|
anabsan2 |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) |