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

Metamath Proof Explorer

Theorem fvreseq1

Description: Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 fnresdm ⊢ ( 𝐺 Fn 𝐵 → ( 𝐺 ↾ 𝐵 ) = 𝐺 )
2 1 ad2antlr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐺 ↾ 𝐵 ) = 𝐺 )
3 2 eqcomd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐺 = ( 𝐺 ↾ 𝐵 ) )
4 3 eqeq2d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) = 𝐺 ↔ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) )
5 ssid ⊢ 𝐵 ⊆ 𝐵
6 fvreseq0 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵 ) ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
7 5 6 mpanr2 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
8 4 7 bitrd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) = 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )