Description: Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013) (Revised by Mario Carneiro, 16-Dec-2013) (Proof shortened by SN, 11-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mpteq2da.1 | |- F/ x ph |
|
| mpteq2da.2 | |- ( ( ph /\ x e. A ) -> B = C ) |
||
| Assertion | mpteq2da | |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpteq2da.1 | |- F/ x ph |
|
| 2 | mpteq2da.2 | |- ( ( ph /\ x e. A ) -> B = C ) |
|
| 3 | eqidd | |- ( ph -> A = A ) |
|
| 4 | 1 3 2 | mpteq12da | |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) ) |