Description: Equality theorem for the Slot construction. The converse holds if A (or B ) is a set. (Contributed by BJ, 27-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sloteq | |- ( 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 ) |