Theorem elnnne0 11933

Description: The positive integer property expressed in terms of difference from zero. (Contributed by Stefan O'Rear, 12-Sep-2015.)

Assertion

Ref	Expression
elnnne0	⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0))

Proof of Theorem elnnne0

Step	Hyp	Ref	Expression
1		dfn2 11932	. . 3 ⊢ ℕ = (ℕ0 ∖ {0})
2	1	eleq2i 2842	. 2 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℕ0 ∖ {0}))
3		eldifsn 4670	. 2 ⊢ (𝑁 ∈ (ℕ0 ∖ {0}) ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0))
4	2, 3	bitri 278	1 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2112   ≠ wne 2949   ∖ cdif 3851  {csn 4515  0cc0 10560  ℕcn 11659  ℕ₀cn0 11919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7146  df-om 7573  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-er 8292  df-en 8521  df-dom 8522  df-sdom 8523  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-nn 11660  df-n0 11920

This theorem is referenced by:  nn0n0n1ge2  11986  nn0nndivcl  11990  fzo1fzo0n0  13122  elfznelfzo  13176  hashnn0n0nn  13787  swrdccatin1  14119  cshwsublen  14190  cshwidxmod  14197  cshwidx0  14200  repswcshw  14206  cshw1  14216  nn0onn  15766  hashfinmndnn  17979  odhash3  18753  prmgrpsimpgd  19289  0ringnnzr  20095  cply1mul  21003  fvmptnn04if  21534  chfacfisf  21539  chfacfisfcpmat  21540  tayl0  25041  dvtaylp  25049  2sqmod  26104  wlkonl1iedg  27539  pthdlem2  27641  crctcsh  27694  clwwlkneq0  27898  hashecclwwlkn1  27946  umgrhashecclwwlk  27947  clwwlknon0  27962  frgrreg  28263  frgrregord013  28264  xnn0gt0  30601  subne0nn  30644  plymulx0  32030  plymulx  32031  signstfvn  32052  signstfveq0a  32059  poimirlem13  35335  poimirlem20  35342  flt0  39951  dvnmul  42936  dvnprodlem3  42941  wallispilem3  43060  fourierdlem103  43202  fourierdlem104  43203  etransclem28  43255  etransclem35  43262  etransclem38  43265  etransclem44  43271  2ffzoeq  44238  lswn0  44314  ztprmneprm  45101