Theorem elnn0

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

	Ref	Expression
Assertion	elnn0	|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		df-n0	|- NN0 = ( NN u. { 0 } )
2	1	eleq2i	|- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun	|- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex	|- 0 e. _V
5	4	elsn2	|- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i	|- ( ( A e. NN \/ A e. { 0 } ) <-> ( A e. NN \/ A = 0 ) )
7	2 3 6	3bitri	|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )