Theorem 4nn0 9225

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 9112	. 2 ⊢ 4 ∈ ℕ
2	1	nnnn0i 9214	1 ⊢ 4 ∈ ℕ0

Syntax hints:   ∈ wcel 2160  4c4 9002  ℕ₀cn0 9206

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4136  ax-cnex 7932  ax-resscn 7933  ax-1re 7935  ax-addrcl 7938

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5899  df-inn 8950  df-2 9008  df-3 9009  df-4 9010  df-n0 9207

This theorem is referenced by:  6p5e11  9486  7p5e12  9490  8p5e13  9496  8p7e15  9498  9p5e14  9503  9p6e15  9504  4t3e12  9511  4t4e16  9512  5t5e25  9516  6t4e24  9519  6t5e30  9520  7t3e21  9523  7t5e35  9525  7t7e49  9527  8t3e24  9529  8t4e32  9530  8t5e40  9531  8t6e48  9532  8t7e56  9533  8t8e64  9534  9t5e45  9538  9t6e54  9539  9t7e63  9540  decbin3  9555  fzo0to42pr  10250  4bc3eq4  10785  resin4p  11758  recos4p  11759  ef01bndlem  11796  sin01bnd  11797  cos01bnd  11798  prm23lt5  12295  slotsdifdsndx  12732  slotsdifunifndx  12739  cnfldstr  13866  binom4  14857  ex-exp  14940  ex-fac  14941  ex-bc  14942