Theorem sadid1

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

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

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A C_ NN0 -> A C_ NN0 )
2		0ss	|- (/) C_ NN0
3	2	a1i	|- ( A C_ NN0 -> (/) C_ NN0 )
4		in0	|- ( A i^i (/) ) = (/)
5	4	a1i	|- ( A C_ NN0 -> ( A i^i (/) ) = (/) )
6	1 3 5	saddisj	|- ( A C_ NN0 -> ( A sadd (/) ) = ( A u. (/) ) )
7		un0	|- ( A u. (/) ) = A
8	6 7	eqtrdi	|- ( A C_ NN0 -> ( A sadd (/) ) = A )