Theorem bj-evalid

Description: The evaluation at a set of the identity function is that set. (General form of ndxarg .) The restriction to a set V is necessary since the argument of the function Slot A (like that of any function) has to be a set for the evaluation to be meaningful. (Contributed by BJ, 27-Dec-2021)

	Ref	Expression
Assertion	bj-evalid	|- ( ( V e. W /\ A e. V ) -> ( Slot A ` ( _I |` V ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		resiexg	|- ( V e. W -> ( _I |` V ) e. _V )
2		bj-evalval	|- ( ( _I |` V ) e. _V -> ( Slot A ` ( _I |` V ) ) = ( ( _I |` V ) ` A ) )
3	1 2	syl	|- ( V e. W -> ( Slot A ` ( _I |` V ) ) = ( ( _I |` V ) ` A ) )
4		fvresi	|- ( A e. V -> ( ( _I |` V ) ` A ) = A )
5	3 4	sylan9eq	|- ( ( V e. W /\ A e. V ) -> ( Slot A ` ( _I |` V ) ) = A )