Theorem 7nn0 11502

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 11378	. 2 ⊢ 7 ∈ ℕ
2	1	nnnn0i 11488	1 ⊢ 7 ∈ ℕ0

Syntax hints:   ∈ wcel 2135  7c7 11263  ℕ₀cn0 11480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-1cn 10182

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-om 7227  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-nn 11209  df-2 11267  df-3 11268  df-4 11269  df-5 11270  df-6 11271  df-7 11272  df-n0 11481

This theorem is referenced by:  7p4e11  11793  7p4e11OLD  11794  7p5e12  11795  7p6e13  11796  7p7e14  11797  8p8e16  11806  9p8e17  11814  9p9e18  11815  7t3e21  11837  7t4e28  11838  7t5e35  11839  7t6e42  11840  7t7e49  11841  8t8e64  11850  9t3e27  11852  9t4e36  11853  9t8e72  11857  9t9e81  11858  7prm  16015  17prm  16022  23prm  16024  prmlem2  16025  37prm  16026  83prm  16028  139prm  16029  163prm  16030  317prm  16031  631prm  16032  1259lem1  16036  1259lem2  16037  1259lem3  16038  1259lem4  16039  1259lem5  16040  1259prm  16041  2503lem1  16042  2503lem2  16043  2503lem3  16044  2503prm  16045  4001lem1  16046  4001lem2  16047  4001lem3  16048  4001lem4  16049  4001prm  16050  quartlem1  24779  quartlem2  24780  log2ublem1  24868  log2ublem3  24870  log2ub  24871  bclbnd  25200  bpos1  25203  ex-prmo  27623  hgt750lemd  31031  hgt750lem  31034  hgt750lem2  31035  hgt750leme  31041  tgoldbachgnn  31042  tgoldbachgtde  31043  tgoldbachgt  31046  expdiophlem2  38087  fmtno5lem2  41972  fmtno5lem4  41974  fmtno5  41975  257prm  41979  fmtno4nprmfac193  41992  fmtno5faclem1  41997  fmtno5faclem2  41998  fmtno5fac  42000  fmtno5nprm  42001  139prmALT  42017  127prm  42021  m11nprm  42024  tgoldbach  42211  tgoldbachOLD  42218