Theorem fun2ssres

Description: Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994)

	Ref	Expression
Assertion	fun2ssres	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺 ) → ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		resabs1	⊢ ( 𝐴 ⊆ dom 𝐺 → ( ( 𝐹 ↾ dom 𝐺 ) ↾ 𝐴 ) = ( 𝐹 ↾ 𝐴 ) )
2	1	eqcomd	⊢ ( 𝐴 ⊆ dom 𝐺 → ( 𝐹 ↾ 𝐴 ) = ( ( 𝐹 ↾ dom 𝐺 ) ↾ 𝐴 ) )
3		funssres	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )
4	3	reseq1d	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ( 𝐹 ↾ dom 𝐺 ) ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) )
5	2 4	sylan9eqr	⊢ ( ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝐴 ⊆ dom 𝐺 ) → ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) )
6	5	3impa	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺 ) → ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) )