Theorem bj-evalidval

Description: Closed general form of strndxid . Both sides are equal to ( FA ) by bj-evalid and bj-evalval respectively, but bj-evalidval adds something to bj-evalid and bj-evalval in that Slot A appears on both sides. (Contributed by BJ, 27-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		bj-evalid	|- ( ( V e. W /\ A e. V ) -> ( Slot A ` ( _I |` V ) ) = A )
2	1	fveq2d	|- ( ( V e. W /\ A e. V ) -> ( F ` ( Slot A ` ( _I |` V ) ) ) = ( F ` A ) )
3	2	3adant3	|- ( ( V e. W /\ A e. V /\ F e. U ) -> ( F ` ( Slot A ` ( _I |` V ) ) ) = ( F ` A ) )
4		bj-evalval	|- ( F e. U -> ( Slot A ` F ) = ( F ` A ) )
5	4	eqcomd	|- ( F e. U -> ( F ` A ) = ( Slot A ` F ) )
6	5	3ad2ant3	|- ( ( V e. W /\ A e. V /\ F e. U ) -> ( F ` A ) = ( Slot A ` F ) )
7	3 6	eqtrd	|- ( ( V e. W /\ A e. V /\ F e. U ) -> ( F ` ( Slot A ` ( _I |` V ) ) ) = ( Slot A ` F ) )