Theorem 4nn0 9168

Description: 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
4nn0	⊢ 4 ∈ ℕ0

Proof of Theorem 4nn0

Step	Hyp	Ref	Expression
1		4nn 9055	. 2 ⊢ 4 ∈ ℕ
2	1	nnnn0i 9157	1 ⊢ 4 ∈ ℕ0

Syntax hints:   ∈ wcel 2146  4c4 8945  ℕ₀cn0 9149

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116  ax-cnex 7877  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-iota 5170  df-fv 5216  df-ov 5868  df-inn 8893  df-2 8951  df-3 8952  df-4 8953  df-n0 9150

This theorem is referenced by:  6p5e11  9429  7p5e12  9433  8p5e13  9439  8p7e15  9441  9p5e14  9446  9p6e15  9447  4t3e12  9454  4t4e16  9455  5t5e25  9459  6t4e24  9462  6t5e30  9463  7t3e21  9466  7t5e35  9468  7t7e49  9470  8t3e24  9472  8t4e32  9473  8t5e40  9474  8t6e48  9475  8t7e56  9476  8t8e64  9477  9t5e45  9481  9t6e54  9482  9t7e63  9483  decbin3  9498  fzo0to42pr  10190  4bc3eq4  10721  resin4p  11694  recos4p  11695  ef01bndlem  11732  sin01bnd  11733  cos01bnd  11734  prm23lt5  12230  slotsdifdsndx  12609  binom4  13968  ex-exp  14039  ex-fac  14040  ex-bc  14041