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	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ‘ ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) ) = ( Slot 𝐴 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-evalid	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) = 𝐴 )
2	1	fveq2d	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ‘ ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) ) = ( 𝐹 ‘ 𝐴 ) )
3	2	3adant3	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ‘ ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) ) = ( 𝐹 ‘ 𝐴 ) )
4		bj-evalval	⊢ ( 𝐹 ∈ 𝑈 → ( Slot 𝐴 ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )
5	4	eqcomd	⊢ ( 𝐹 ∈ 𝑈 → ( 𝐹 ‘ 𝐴 ) = ( Slot 𝐴 ‘ 𝐹 ) )
6	5	3ad2ant3	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ‘ 𝐴 ) = ( Slot 𝐴 ‘ 𝐹 ) )
7	3 6	eqtrd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ‘ ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) ) = ( Slot 𝐴 ‘ 𝐹 ) )