Theorem 2nn0 9018

Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
2nn0	⊢ 2 ∈ ℕ0

Proof of Theorem 2nn0

Step	Hyp	Ref	Expression
1		2nn 8905	. 2 ⊢ 2 ∈ ℕ
2	1	nnnn0i 9009	1 ⊢ 2 ∈ ℕ0

Syntax hints:   ∈ wcel 1481  2c2 8795  ℕ₀cn0 9001

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-cnex 7735  ax-resscn 7736  ax-1re 7738  ax-addrcl 7741

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785  df-inn 8745  df-2 8803  df-n0 9002

This theorem is referenced by:  nn0n0n1ge2  9145  7p6e13  9283  8p3e11  9286  8p5e13  9288  9p3e12  9293  9p4e13  9294  4t3e12  9303  4t4e16  9304  5t3e15  9306  5t5e25  9308  6t3e18  9310  6t5e30  9312  7t3e21  9315  7t4e28  9316  7t5e35  9317  7t6e42  9318  7t7e49  9319  8t3e24  9321  8t4e32  9322  8t5e40  9323  9t3e27  9328  9t4e36  9329  9t8e72  9333  9t9e81  9334  decbin3  9347  2eluzge0  9397  nn01to3  9436  xnn0le2is012  9679  fzo0to42pr  10028  nn0sqcl  10351  sqmul  10386  resqcl  10391  zsqcl  10394  cu2  10422  i3  10425  i4  10426  binom3  10440  nn0opthlem1d  10498  fac3  10510  faclbnd2  10520  abssq  10885  sqabs  10886  ef4p  11437  efgt1p2  11438  efi4p  11460  ef01bndlem  11499  cos01bnd  11501  oexpneg  11610  oddge22np1  11614  setsmsdsg  12688  dveflem  12895  tangtx  12967  2logb9irr  13096  2logb9irrap  13102  1kp2ke3k  13107  ex-exp  13110  ex-fac  13111