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 𝐵 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) = 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )