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