Theorem funssfv

Description: The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994)

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

Proof

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