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

Metamath Proof Explorer

Theorem fvreseq0

Description: Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019)

Ref Expression
Assertion fvreseq0 ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 fnssres ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
2 fnssres ⊢ ( ( 𝐺 Fn 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐺 ↾ 𝐵 ) Fn 𝐵 )
3 eqfnfv ⊢ ( ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ∧ ( 𝐺 ↾ 𝐵 ) Fn 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) ) )
4 fvres ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
5 fvres ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
6 4 5 eqeq12d ⊢ ( 𝑥 ∈ 𝐵 → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
7 6 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
8 3 7 bitrdi ⊢ ( ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ∧ ( 𝐺 ↾ 𝐵 ) Fn 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
9 1 2 8 syl2an ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐺 Fn 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
10 9 an4s ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )