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 | |- ( F e. V -> ( Slot A ` F ) = ( F ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex | |- ( F e. V -> F e. _V ) |
|
| 2 | fveq1 | |- ( f = F -> ( f ` A ) = ( F ` A ) ) |
|
| 3 | df-slot | |- Slot A = ( f e. _V |-> ( f ` A ) ) |
|
| 4 | fvex | |- ( F ` A ) e. _V |
|
| 5 | 2 3 4 | fvmpt | |- ( F e. _V -> ( Slot A ` F ) = ( F ` A ) ) |
| 6 | 1 5 | syl | |- ( F e. V -> ( Slot A ` F ) = ( F ` A ) ) |