Theorem sadid2

Description: The adder sequence function has a right identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Assertion	sadid2	|- ( A C_ NN0 -> ( (/) sadd A ) = A )

Proof

Step	Hyp	Ref	Expression
1		0ss	|- (/) C_ NN0
2		sadcom	|- ( ( (/) C_ NN0 /\ A C_ NN0 ) -> ( (/) sadd A ) = ( A sadd (/) ) )
3	1 2	mpan	|- ( A C_ NN0 -> ( (/) sadd A ) = ( A sadd (/) ) )
4		sadid1	|- ( A C_ NN0 -> ( A sadd (/) ) = A )
5	3 4	eqtrd	|- ( A C_ NN0 -> ( (/) sadd A ) = A )