Metamath Proof Explorer

Theorem subid1

Description: Identity law for subtraction. (Contributed by NM, 9-May-2004) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion subid1 
|- ( A e. CC -> ( A - 0 ) = A )

Proof

Step Hyp Ref Expression
1 addid1 
 |-  ( A e. CC -> ( A + 0 ) = A )
2 1 oveq1d 
 |-  ( A e. CC -> ( ( A + 0 ) - 0 ) = ( A - 0 ) )
3 0cn 
 |-  0 e. CC
4 pncan 
 |-  ( ( A e. CC /\ 0 e. CC ) -> ( ( A + 0 ) - 0 ) = A )
5 3 4 mpan2 
 |-  ( A e. CC -> ( ( A + 0 ) - 0 ) = A )
6 2 5 eqtr3d 
 |-  ( A e. CC -> ( A - 0 ) = A )