Theorem 6nn0 9173

Description: 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Assertion

Ref	Expression
6nn0	|- 6 e. NN0

Proof of Theorem 6nn0

Step	Hyp	Ref	Expression
1		6nn 9060	. 2 |- 6 e. NN
2	1	nnnn0i 9160	1 |- 6 e. NN0

Syntax hints:   e. wcel 2148   6c6 8950   NN0cn0 9152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4118  ax-cnex 7880  ax-resscn 7881  ax-1re 7883  ax-addrcl 7886

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-iota 5173  df-fv 5219  df-ov 5871  df-inn 8896  df-2 8954  df-3 8955  df-4 8956  df-5 8957  df-6 8958  df-n0 9153

This theorem is referenced by:  6p5e11  9432  6p6e12  9433  7p7e14  9438  8p7e15  9444  9p7e16  9451  9p8e17  9452  6t3e18  9464  6t4e24  9465  6t5e30  9466  6t6e36  9467  7t7e49  9473  8t3e24  9475  8t7e56  9479  8t8e64  9480  9t4e36  9483  9t5e45  9484  9t7e63  9486  9t8e72  9487  6lcm4e12  12057  slotsdnscsi  12620  ex-exp  14101