Theorem 5nn0 9159

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

Assertion

Ref	Expression
5nn0	|- 5 e. NN0

Proof of Theorem 5nn0

Step	Hyp	Ref	Expression
1		5nn 9046	. 2 |- 5 e. NN
2	1	nnnn0i 9147	1 |- 5 e. NN0

Syntax hints:   e. wcel 2142   5c5 8936   NN0cn0 9139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153  ax-sep 4108  ax-cnex 7869  ax-resscn 7870  ax-1re 7872  ax-addrcl 7875

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-un 3126  df-in 3128  df-ss 3135  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-br 3991  df-iota 5162  df-fv 5208  df-ov 5860  df-inn 8883  df-2 8941  df-3 8942  df-4 8943  df-5 8944  df-n0 9140

This theorem is referenced by:  6p6e12  9420  7p6e13  9424  8p6e14  9430  8p8e16  9432  9p6e15  9437  9p7e16  9438  5t2e10  9446  5t3e15  9447  5t4e20  9448  5t5e25  9449  6t6e36  9454  7t5e35  9458  7t6e42  9459  8t6e48  9465  8t8e64  9467  9t5e45  9471  9t6e54  9472  9t7e63  9473  ex-fac  13848