Theorem pinn 7492

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 7487	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3330	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3256	. 2 ⊢ N ⊆ ω
4	3	sseli 3220	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2200   ∖ cdif 3194  ∅c0 3491  {csn 3666  ωcom 4681  Ncnpi 7455

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-in 3203  df-ss 3210  df-ni 7487

This theorem is referenced by:  pion  7493  piord  7494  elni2  7497  mulidpi  7501  ltsopi  7503  pitric  7504  pitri3or  7505  ltdcpi  7506  addclpi  7510  mulclpi  7511  addcompig  7512  addasspig  7513  mulcompig  7514  mulasspig  7515  distrpig  7516  addcanpig  7517  mulcanpig  7518  addnidpig  7519  ltexpi  7520  ltapig  7521  ltmpig  7522  nnppipi  7526  enqdc  7544  archnqq  7600  prarloclemarch2  7602  enq0enq  7614  enq0sym  7615  enq0ref  7616  enq0tr  7617  nqnq0pi  7621  nqnq0  7624  addcmpblnq0  7626  mulcmpblnq0  7627  mulcanenq0ec  7628  addclnq0  7634  nqpnq0nq  7636  nqnq0a  7637  nqnq0m  7638  nq0m0r  7639  nq0a0  7640  nnanq0  7641  distrnq0  7642  mulcomnq0  7643  addassnq0lemcl  7644  addassnq0  7645  nq02m  7648  prarloclemlt  7676  prarloclemn  7682