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	⊢ ( 𝐴 ⊆ ℕ0 → ( ∅ sadd 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ℕ0
2		sadcom	⊢ ( ( ∅ ⊆ ℕ0 ∧ 𝐴 ⊆ ℕ0 ) → ( ∅ sadd 𝐴 ) = ( 𝐴 sadd ∅ ) )
3	1 2	mpan	⊢ ( 𝐴 ⊆ ℕ0 → ( ∅ sadd 𝐴 ) = ( 𝐴 sadd ∅ ) )
4		sadid1	⊢ ( 𝐴 ⊆ ℕ0 → ( 𝐴 sadd ∅ ) = 𝐴 )
5	3 4	eqtrd	⊢ ( 𝐴 ⊆ ℕ0 → ( ∅ sadd 𝐴 ) = 𝐴 )