Description: Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999) (Revised by Mario Carneiro, 27-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | subid | |- ( A e. CC -> ( A - A ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | addid1 | |- ( A e. CC -> ( A + 0 ) = A ) |
|
| 2 | 1 | oveq1d | |- ( A e. CC -> ( ( A + 0 ) - A ) = ( A - A ) ) |
| 3 | 0cn | |- 0 e. CC |
|
| 4 | pncan2 | |- ( ( A e. CC /\ 0 e. CC ) -> ( ( A + 0 ) - A ) = 0 ) |
|
| 5 | 3 4 | mpan2 | |- ( A e. CC -> ( ( A + 0 ) - A ) = 0 ) |
| 6 | 2 5 | eqtr3d | |- ( A e. CC -> ( A - A ) = 0 ) |