Theorem pinn 7271

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 7266	. . 3 |- N. = ( om \ { (/) } )
2		difss 3253	. . 3 |- ( om \ { (/) } ) C_ om
3	1, 2	eqsstri 3179	. 2 |- N. C_ om
4	3	sseli 3143	1 |- ( A e. N. -> A e. om )

Syntax hints:   -> wi 4   e. wcel 2141   \ cdif 3118   (/)c0 3414   {csn 3583   omcom 4574   N.cnpi 7234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-in 3127  df-ss 3134  df-ni 7266

This theorem is referenced by:  pion  7272  piord  7273  elni2  7276  mulidpi  7280  ltsopi  7282  pitric  7283  pitri3or  7284  ltdcpi  7285  addclpi  7289  mulclpi  7290  addcompig  7291  addasspig  7292  mulcompig  7293  mulasspig  7294  distrpig  7295  addcanpig  7296  mulcanpig  7297  addnidpig  7298  ltexpi  7299  ltapig  7300  ltmpig  7301  nnppipi  7305  enqdc  7323  archnqq  7379  prarloclemarch2  7381  enq0enq  7393  enq0sym  7394  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  nqnq0  7403  addcmpblnq0  7405  mulcmpblnq0  7406  mulcanenq0ec  7407  addclnq0  7413  nqpnq0nq  7415  nqnq0a  7416  nqnq0m  7417  nq0m0r  7418  nq0a0  7419  nnanq0  7420  distrnq0  7421  mulcomnq0  7422  addassnq0lemcl  7423  addassnq0  7424  nq02m  7427  prarloclemlt  7455  prarloclemn  7461