Theorem pinn 7404

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 7399	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3298	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3224	. 2 ⊢ N ⊆ ω
4	3	sseli 3188	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2175   ∖ cdif 3162  ∅c0 3459  {csn 3632  ωcom 4636  Ncnpi 7367

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 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-dif 3167  df-in 3171  df-ss 3178  df-ni 7399

This theorem is referenced by:  pion  7405  piord  7406  elni2  7409  mulidpi  7413  ltsopi  7415  pitric  7416  pitri3or  7417  ltdcpi  7418  addclpi  7422  mulclpi  7423  addcompig  7424  addasspig  7425  mulcompig  7426  mulasspig  7427  distrpig  7428  addcanpig  7429  mulcanpig  7430  addnidpig  7431  ltexpi  7432  ltapig  7433  ltmpig  7434  nnppipi  7438  enqdc  7456  archnqq  7512  prarloclemarch2  7514  enq0enq  7526  enq0sym  7527  enq0ref  7528  enq0tr  7529  nqnq0pi  7533  nqnq0  7536  addcmpblnq0  7538  mulcmpblnq0  7539  mulcanenq0ec  7540  addclnq0  7546  nqpnq0nq  7548  nqnq0a  7549  nqnq0m  7550  nq0m0r  7551  nq0a0  7552  nnanq0  7553  distrnq0  7554  mulcomnq0  7555  addassnq0lemcl  7556  addassnq0  7557  nq02m  7560  prarloclemlt  7588  prarloclemn  7594