Theorem fvreseq

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