Theorem pinn 7589

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 7584	. . 3 |- N. = ( om \ { (/) } )
2		difss 3335	. . 3 |- ( om \ { (/) } ) C_ om
3	1, 2	eqsstri 3260	. 2 |- N. C_ om
4	3	sseli 3224	1 |- ( A e. N. -> A e. om )

Syntax hints:   -> wi 4   e. wcel 2202   \ cdif 3198   (/)c0 3496   {csn 3673   omcom 4694   N.cnpi 7552

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 7584

This theorem is referenced by:  pion  7590  piord  7591  elni2  7594  mulidpi  7598  ltsopi  7600  pitric  7601  pitri3or  7602  ltdcpi  7603  addclpi  7607  mulclpi  7608  addcompig  7609  addasspig  7610  mulcompig  7611  mulasspig  7612  distrpig  7613  addcanpig  7614  mulcanpig  7615  addnidpig  7616  ltexpi  7617  ltapig  7618  ltmpig  7619  nnppipi  7623  enqdc  7641  archnqq  7697  prarloclemarch2  7699  enq0enq  7711  enq0sym  7712  enq0ref  7713  enq0tr  7714  nqnq0pi  7718  nqnq0  7721  addcmpblnq0  7723  mulcmpblnq0  7724  mulcanenq0ec  7725  addclnq0  7731  nqpnq0nq  7733  nqnq0a  7734  nqnq0m  7735  nq0m0r  7736  nq0a0  7737  nnanq0  7738  distrnq0  7739  mulcomnq0  7740  addassnq0lemcl  7741  addassnq0  7742  nq02m  7745  prarloclemlt  7773  prarloclemn  7779