Theorem pinn 7572

Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)

Assertion

Ref	Expression
pinn	⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Proof of Theorem pinn

Step	Hyp	Ref	Expression
1		df-ni 7567	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3335	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3260	. 2 ⊢ N ⊆ ω
4	3	sseli 3224	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2202   ∖ cdif 3198  ∅c0 3496  {csn 3673  ωcom 4694  Ncnpi 7535

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-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-dif 3203  df-in 3207  df-ss 3214  df-ni 7567

This theorem is referenced by:  pion  7573  piord  7574  elni2  7577  mulidpi  7581  ltsopi  7583  pitric  7584  pitri3or  7585  ltdcpi  7586  addclpi  7590  mulclpi  7591  addcompig  7592  addasspig  7593  mulcompig  7594  mulasspig  7595  distrpig  7596  addcanpig  7597  mulcanpig  7598  addnidpig  7599  ltexpi  7600  ltapig  7601  ltmpig  7602  nnppipi  7606  enqdc  7624  archnqq  7680  prarloclemarch2  7682  enq0enq  7694  enq0sym  7695  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  nqnq0  7704  addcmpblnq0  7706  mulcmpblnq0  7707  mulcanenq0ec  7708  addclnq0  7714  nqpnq0nq  7716  nqnq0a  7717  nqnq0m  7718  nq0m0r  7719  nq0a0  7720  nnanq0  7721  distrnq0  7722  mulcomnq0  7723  addassnq0lemcl  7724  addassnq0  7725  nq02m  7728  prarloclemlt  7756  prarloclemn  7762