Theorem fvres

Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	fvres	|- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	brresi	|- ( A ( F |` B ) x <-> ( A e. B /\ A F x ) )
3	2	baib	|- ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
4	3	iotabidv	|- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv	|- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv	|- ( F ` A ) = ( iota x A F x )
7	4 5 6	3eqtr4g	|- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )