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 AA0=A

Proof

Step Hyp Ref Expression
1 addid1 AA+0=A
2 1 oveq1d AA+0-0=A0
3 0cn 0
4 pncan A0A+0-0=A
5 3 4 mpan2 AA+0-0=A
6 2 5 eqtr3d AA0=A