Theorem subsid1

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

	Ref	Expression
Assertion	subsid1	$$⊢A\in \mathrm{No}\to A{-}_s{0}_s=A$$

Proof

Step	Hyp	Ref	Expression
1		0sno	$$⊢0_s\in \mathrm{No}$$
2		subsval	$$⊢\left(A\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to A{-}_s{0}_s=A{+}_s{+}_s\left(0_s\right)$$
3	1 2	mpan2	$$⊢A\in \mathrm{No}\to A{-}_s{0}_s=A{+}_s{+}_s\left(0_s\right)$$
4		negs0s	$$⊢{+}_s\left(0_s\right)=0_s$$
5	4	oveq2i	$$⊢A{+}_s{+}_s\left(0_s\right)=A{+}_s{0}_s$$
6		addsrid	$$⊢A\in \mathrm{No}\to A{+}_s{0}_s=A$$
7	5 6	eqtrid	$$⊢A\in \mathrm{No}\to A{+}_s{+}_s\left(0_s\right)=A$$
8	3 7	eqtrd	$$⊢A\in \mathrm{No}\to A{-}_s{0}_s=A$$