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 ) ) |