Theorem fvresval

Description: The value of a function at a restriction is either null or the same as the function itself. (Contributed by Scott Fenton, 4-Sep-2011)

	Ref	Expression
Assertion	fvresval	|- ( ( ( F |` B ) ` A ) = ( F ` A ) \/ ( ( F |` B ) ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		exmid	|- ( A e. B \/ -. A e. B )
2		fvres	|- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )
3		nfvres	|- ( -. A e. B -> ( ( F |` B ) ` A ) = (/) )
4	2 3	orim12i	|- ( ( A e. B \/ -. A e. B ) -> ( ( ( F |` B ) ` A ) = ( F ` A ) \/ ( ( F |` B ) ` A ) = (/) ) )
5	1 4	ax-mp	|- ( ( ( F |` B ) ` A ) = ( F ` A ) \/ ( ( F |` B ) ` A ) = (/) )