Theorem elnn0

Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Assertion	elnn0	⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		df-n0	⊢ ℕ0 = ( ℕ ∪ { 0 } )
2	1	eleq2i	⊢ ( 𝐴 ∈ ℕ0 ↔ 𝐴 ∈ ( ℕ ∪ { 0 } ) )
3		elun	⊢ ( 𝐴 ∈ ( ℕ ∪ { 0 } ) ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 ∈ { 0 } ) )
4		c0ex	⊢ 0 ∈ V
5	4	elsn2	⊢ ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 )
6	5	orbi2i	⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 ∈ { 0 } ) ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
7	2 3 6	3bitri	⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )