Theorem pinn 7496

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

Assertion

Ref	Expression
pinn	|- ( A e. N. -> A e. om )

Proof of Theorem pinn

Step	Hyp	Ref	Expression
1		df-ni 7491	. . 3 |- N. = ( om \ { (/) } )
2		difss 3330	. . 3 |- ( om \ { (/) } ) C_ om
3	1, 2	eqsstri 3256	. 2 |- N. C_ om
4	3	sseli 3220	1 |- ( A e. N. -> A e. om )

Syntax hints:   -> wi 4   e. wcel 2200   \ cdif 3194   (/)c0 3491   {csn 3666   omcom 4682   N.cnpi 7459

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 7491

This theorem is referenced by:  pion  7497  piord  7498  elni2  7501  mulidpi  7505  ltsopi  7507  pitric  7508  pitri3or  7509  ltdcpi  7510  addclpi  7514  mulclpi  7515  addcompig  7516  addasspig  7517  mulcompig  7518  mulasspig  7519  distrpig  7520  addcanpig  7521  mulcanpig  7522  addnidpig  7523  ltexpi  7524  ltapig  7525  ltmpig  7526  nnppipi  7530  enqdc  7548  archnqq  7604  prarloclemarch2  7606  enq0enq  7618  enq0sym  7619  enq0ref  7620  enq0tr  7621  nqnq0pi  7625  nqnq0  7628  addcmpblnq0  7630  mulcmpblnq0  7631  mulcanenq0ec  7632  addclnq0  7638  nqpnq0nq  7640  nqnq0a  7641  nqnq0m  7642  nq0m0r  7643  nq0a0  7644  nnanq0  7645  distrnq0  7646  mulcomnq0  7647  addassnq0lemcl  7648  addassnq0  7649  nq02m  7652  prarloclemlt  7680  prarloclemn  7686