Theorem fssres2

Description: Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005)

	Ref	Expression
Assertion	fssres2	|- ( ( ( F |` A ) : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )

Proof

Step	Hyp	Ref	Expression
1		fssres	|- ( ( ( F |` A ) : A --> B /\ C C_ A ) -> ( ( F |` A ) |` C ) : C --> B )
2		resabs1	|- ( C C_ A -> ( ( F |` A ) |` C ) = ( F |` C ) )
3	2	feq1d	|- ( C C_ A -> ( ( ( F |` A ) |` C ) : C --> B <-> ( F |` C ) : C --> B ) )
4	3	adantl	|- ( ( ( F |` A ) : A --> B /\ C C_ A ) -> ( ( ( F |` A ) |` C ) : C --> B <-> ( F |` C ) : C --> B ) )
5	1 4	mpbid	|- ( ( ( F |` A ) : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )