Theorem 7nn0 11566

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

Assertion

Ref	Expression
7nn0	⊢ 7 ∈ ℕ0

Proof of Theorem 7nn0

Step	Hyp	Ref	Expression
1		7nn 11372	. 2 ⊢ 7 ∈ ℕ
2	1	nnnn0i 11551	1 ⊢ 7 ∈ ℕ0

Syntax hints:   ∈ wcel 2155  7c7 11336  ℕ₀cn0 11542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-1cn 10251

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6849  df-om 7268  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-n0 11543

This theorem is referenced by:  7p4e11  11822  7p5e12  11823  7p6e13  11824  7p7e14  11825  8p8e16  11832  9p8e17  11839  9p9e18  11840  7t3e21  11856  7t4e28  11857  7t5e35  11858  7t6e42  11859  7t7e49  11860  8t8e64  11867  9t3e27  11869  9t4e36  11870  9t8e72  11874  9t9e81  11875  7prm  16105  17prm  16111  23prm  16113  prmlem2  16114  37prm  16115  83prm  16117  139prm  16118  163prm  16119  317prm  16120  631prm  16121  1259lem1  16125  1259lem2  16126  1259lem3  16127  1259lem4  16128  1259lem5  16129  1259prm  16130  2503lem1  16131  2503lem2  16132  2503lem3  16133  2503prm  16134  4001lem1  16135  4001lem2  16136  4001lem3  16137  4001lem4  16138  4001prm  16139  quartlem1  24889  quartlem2  24890  log2ublem1  24978  log2ublem3  24980  log2ub  24981  bclbnd  25310  bpos1  25313  ex-prmo  27796  hgt750lemd  31198  hgt750lem  31201  hgt750lem2  31202  hgt750leme  31208  tgoldbachgnn  31209  tgoldbachgtde  31210  tgoldbachgt  31213  expdiophlem2  38290  fmtno5lem2  42166  fmtno5lem4  42168  fmtno5  42169  257prm  42173  fmtno4nprmfac193  42186  fmtno5faclem1  42191  fmtno5faclem2  42192  fmtno5fac  42194  fmtno5nprm  42195  139prmALT  42211  127prm  42215  m11nprm  42218  tgoldbach  42405