Description: Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | resubidaddid1 | |- ( ( A e. RR /\ B e. RR ) -> ( ( A -R A ) + B ) = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | readdsub | |- ( ( A e. RR /\ B e. RR /\ A e. RR ) -> ( ( A + B ) -R A ) = ( ( A -R A ) + B ) ) |
|
2 | 1 | 3anidm13 | |- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) -R A ) = ( ( A -R A ) + B ) ) |
3 | repncan2 | |- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) -R A ) = B ) |
|
4 | 2 3 | eqtr3d | |- ( ( A e. RR /\ B e. RR ) -> ( ( A -R A ) + B ) = B ) |