Metamath Proof Explorer


Theorem subsid1

Description: Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion subsid1 A No A - s 0 s = A

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 subsval A No 0 s No A - s 0 s = A + s + s 0 s
3 1 2 mpan2 A No A - s 0 s = A + s + s 0 s
4 negs0s + s 0 s = 0 s
5 4 oveq2i A + s + s 0 s = A + s 0 s
6 addsrid A No A + s 0 s = A
7 5 6 eqtrid A No A + s + s 0 s = A
8 3 7 eqtrd A No A - s 0 s = A