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\subseteq {\mathbb{N}}_0\to A\mathrm{sadd}\varnothing =A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\subseteq {\mathbb{N}}_0\to A\subseteq {\mathbb{N}}_0$$
2		0ss	$$⊢\varnothing \subseteq {\mathbb{N}}_0$$
3	2	a1i	$$⊢A\subseteq {\mathbb{N}}_0\to \varnothing \subseteq {\mathbb{N}}_0$$
4		in0	$$⊢A\cap \varnothing =\varnothing$$
5	4	a1i	$$⊢A\subseteq {\mathbb{N}}_0\to A\cap \varnothing =\varnothing$$
6	1 3 5	saddisj	$$⊢A\subseteq {\mathbb{N}}_0\to A\mathrm{sadd}\varnothing =A\cup \varnothing$$
7		un0	$$⊢A\cup \varnothing =A$$
8	6 7	eqtrdi	$$⊢A\subseteq {\mathbb{N}}_0\to A\mathrm{sadd}\varnothing =A$$