Metamath Proof Explorer


Theorem bj-evalval

Description: Value of the evaluation at a class. (Closed form of strfvnd and strfvn ). (Contributed by NM, 9-Sep-2011) (Revised by Mario Carneiro, 15-Nov-2014) (Revised by BJ, 27-Dec-2021)

Ref Expression
Assertion bj-evalval ( 𝐹𝑉 → ( Slot 𝐴𝐹 ) = ( 𝐹𝐴 ) )

Proof

Step Hyp Ref Expression
1 elex ( 𝐹𝑉𝐹 ∈ V )
2 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝐴 ) = ( 𝐹𝐴 ) )
3 df-slot Slot 𝐴 = ( 𝑓 ∈ V ↦ ( 𝑓𝐴 ) )
4 fvex ( 𝐹𝐴 ) ∈ V
5 2 3 4 fvmpt ( 𝐹 ∈ V → ( Slot 𝐴𝐹 ) = ( 𝐹𝐴 ) )
6 1 5 syl ( 𝐹𝑉 → ( Slot 𝐴𝐹 ) = ( 𝐹𝐴 ) )