Theorem fun2ssres

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

	Ref	Expression
Assertion	fun2ssres	|- ( ( Fun F /\ G C_ F /\ A C_ dom G ) -> ( F |` A ) = ( G |` A ) )

Proof

Step	Hyp	Ref	Expression
1		resabs1	|- ( A C_ dom G -> ( ( F |` dom G ) |` A ) = ( F |` A ) )
2	1	eqcomd	|- ( A C_ dom G -> ( F |` A ) = ( ( F |` dom G ) |` A ) )
3		funssres	|- ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G )
4	3	reseq1d	|- ( ( Fun F /\ G C_ F ) -> ( ( F |` dom G ) |` A ) = ( G |` A ) )
5	2 4	sylan9eqr	|- ( ( ( Fun F /\ G C_ F ) /\ A C_ dom G ) -> ( F |` A ) = ( G |` A ) )
6	5	3impa	|- ( ( Fun F /\ G C_ F /\ A C_ dom G ) -> ( F |` A ) = ( G |` A ) )