Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mpteq1i.1 | |- A = B |
|
| Assertion | mpteq1i | |- ( x e. A |-> C ) = ( x e. B |-> C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpteq1i.1 | |- A = B |
|
| 2 | 1 | a1i | |- ( T. -> A = B ) |
| 3 | eqidd | |- ( T. -> C = C ) |
|
| 4 | 2 3 | mpteq12dv | |- ( T. -> ( x e. A |-> C ) = ( x e. B |-> C ) ) |
| 5 | 4 | mptru | |- ( x e. A |-> C ) = ( x e. B |-> C ) |