Theorem 9nn0 8899

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

Assertion

Ref	Expression
9nn0	|- 9 e. NN0

Proof of Theorem 9nn0

Step	Hyp	Ref	Expression
1		9nn 8786	. 2 |- 9 e. NN
2	1	nnnn0i 8883	1 |- 9 e. NN0

Syntax hints:   e. wcel 1461   9c9 8682   NN0cn0 8875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-cnex 7630  ax-resscn 7631  ax-1re 7633  ax-addrcl 7636

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-br 3894  df-iota 5044  df-fv 5087  df-ov 5729  df-inn 8625  df-2 8683  df-3 8684  df-4 8685  df-5 8686  df-6 8687  df-7 8688  df-8 8689  df-9 8690  df-n0 8876

This theorem is referenced by:  deccl  9094  le9lt10  9106  decsucc  9120  9p2e11  9166  9p3e12  9167  9p4e13  9168  9p5e14  9169  9p6e15  9170  9p7e16  9171  9p8e17  9172  9p9e18  9173  9t3e27  9202  9t4e36  9203  9t5e45  9204  9t6e54  9205  9t7e63  9206  9t8e72  9207  9t9e81  9208  sq10e99m1  10347  3dvds2dec  11405  setsmsdsg  12463