Theorem nn0ex 9321

Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.)

Assertion

Ref	Expression
nn0ex	⊢ ℕ0 ∈ V

Proof of Theorem nn0ex

Step	Hyp	Ref	Expression
1		df-n0 9316	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 9062	. . 3 ⊢ ℕ ∈ V
3		c0ex 8086	. . . 4 ⊢ 0 ∈ V
4	3	snex 4237	. . 3 ⊢ {0} ∈ V
5	2, 4	unex 4496	. 2 ⊢ (ℕ ∪ {0}) ∈ V
6	1, 5	eqeltri 2279	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2177  Vcvv 2773   ∪ cun 3168  {csn 3638  0cc0 7945  ℕcn 9056  ℕ₀cn0 9315

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261  ax-un 4488  ax-cnex 8036  ax-resscn 8037  ax-1cn 8038  ax-1re 8039  ax-icn 8040  ax-addcl 8041  ax-addrcl 8042  ax-mulcl 8043  ax-i2m1 8050

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-uni 3857  df-int 3892  df-inn 9057  df-n0 9316

This theorem is referenced by:  nn0ennn  10600  nnenom  10601  uzennn  10603  xnn0nnen  10604  wrdexg  11027  expcnvap0  11888  expcnvre  11889  expcnv  11890  geolim  11897  mertenslem2  11922  eftlub  12076  bitsfval  12328  bitsf  12332  1arith  12765  znnen  12844  psrval  14503  fnpsr  14504  psrbag  14506  psrbasg  14511  psrelbas  14512  psrplusgg  14515  psraddcl  14517  psr0cl  14518  psr0lid  14519  psrnegcl  14520  psrlinv  14521  psrgrp  14522  psr1clfi  14525  mplsubgfilemm  14535  mplsubgfilemcl  14536  plyval  15279  elply2  15282  plyf  15284  elplyr  15287  plyaddlem1  15294  plyaddlem  15296  plymullem  15297  plyco  15306  plycj  15308  plyrecj  15310