Theorem pinn 7504

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 7499	. . 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 7467

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 7499

This theorem is referenced by:  pion  7505  piord  7506  elni2  7509  mulidpi  7513  ltsopi  7515  pitric  7516  pitri3or  7517  ltdcpi  7518  addclpi  7522  mulclpi  7523  addcompig  7524  addasspig  7525  mulcompig  7526  mulasspig  7527  distrpig  7528  addcanpig  7529  mulcanpig  7530  addnidpig  7531  ltexpi  7532  ltapig  7533  ltmpig  7534  nnppipi  7538  enqdc  7556  archnqq  7612  prarloclemarch2  7614  enq0enq  7626  enq0sym  7627  enq0ref  7628  enq0tr  7629  nqnq0pi  7633  nqnq0  7636  addcmpblnq0  7638  mulcmpblnq0  7639  mulcanenq0ec  7640  addclnq0  7646  nqpnq0nq  7648  nqnq0a  7649  nqnq0m  7650  nq0m0r  7651  nq0a0  7652  nnanq0  7653  distrnq0  7654  mulcomnq0  7655  addassnq0lemcl  7656  addassnq0  7657  nq02m  7660  prarloclemlt  7688  prarloclemn  7694