Theorem bnj1536

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1536.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	bnj1536.2	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
	bnj1536.3	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
	bnj1536.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
Assertion	bnj1536	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1536.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		bnj1536.2	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
3		bnj1536.3	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
4		bnj1536.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
5		fvreseq	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
6	1 2 3 5	syl21anc	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
7	4 6	mpbird	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) )