Description: Equality theorem for the Slot construction. This is currently a duplicate of sloteq but may diverge from it if/when a token Eval is introduced for evaluation in order to separate it from Slot and any of its possible modifications. (Contributed by BJ, 27-Dec-2021) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-evaleq | |- ( A = B -> Slot A = Slot B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 | |- ( A = B -> ( f ` A ) = ( f ` B ) ) |
|
| 2 | 1 | mpteq2dv | |- ( A = B -> ( f e. _V |-> ( f ` A ) ) = ( f e. _V |-> ( f ` B ) ) ) |
| 3 | df-slot | |- Slot A = ( f e. _V |-> ( f ` A ) ) |
|
| 4 | df-slot | |- Slot B = ( f e. _V |-> ( f ` B ) ) |
|
| 5 | 2 3 4 | 3eqtr4g | |- ( A = B -> Slot A = Slot B ) |