Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 16-Dec-2013) Drop ax-10 while shortening its proof. (Revised by Steven Nguyen and Gino Giotto, 1-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mpteq12dv.1 | |- ( ph -> A = C ) |
|
| mpteq12dv.2 | |- ( ph -> B = D ) |
||
| Assertion | mpteq12dv | |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpteq12dv.1 | |- ( ph -> A = C ) |
|
| 2 | mpteq12dv.2 | |- ( ph -> B = D ) |
|
| 3 | nfv | |- F/ x ph |
|
| 4 | 3 1 2 | mpteq12df | |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) ) |