Theorem fvtresfn

Description: Functionality of a tuple-restriction function. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypothesis	fvtresfn.f	|- F = ( x e. B |-> ( x |` V ) )
Assertion	fvtresfn	|- ( X e. B -> ( F ` X ) = ( X |` V ) )

Proof

Step	Hyp	Ref	Expression
1		fvtresfn.f	|- F = ( x e. B |-> ( x |` V ) )
2		resexg	|- ( X e. B -> ( X |` V ) e. _V )
3		reseq1	|- ( x = X -> ( x |` V ) = ( X |` V ) )
4	3 1	fvmptg	|- ( ( X e. B /\ ( X |` V ) e. _V ) -> ( F ` X ) = ( X |` V ) )
5	2 4	mpdan	|- ( X e. B -> ( F ` X ) = ( X |` V ) )