Theorem pinn 7117

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 7112	. . 3 |- N. = ( om \ { (/) } )
2		difss 3202	. . 3 |- ( om \ { (/) } ) C_ om
3	1, 2	eqsstri 3129	. 2 |- N. C_ om
4	3	sseli 3093	1 |- ( A e. N. -> A e. om )

Syntax hints:   -> wi 4   e. wcel 1480   \ cdif 3068   (/)c0 3363   {csn 3527   omcom 4504   N.cnpi 7080

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-dif 3073  df-in 3077  df-ss 3084  df-ni 7112

This theorem is referenced by:  pion  7118  piord  7119  elni2  7122  mulidpi  7126  ltsopi  7128  pitric  7129  pitri3or  7130  ltdcpi  7131  addclpi  7135  mulclpi  7136  addcompig  7137  addasspig  7138  mulcompig  7139  mulasspig  7140  distrpig  7141  addcanpig  7142  mulcanpig  7143  addnidpig  7144  ltexpi  7145  ltapig  7146  ltmpig  7147  nnppipi  7151  enqdc  7169  archnqq  7225  prarloclemarch2  7227  enq0enq  7239  enq0sym  7240  enq0ref  7241  enq0tr  7242  nqnq0pi  7246  nqnq0  7249  addcmpblnq0  7251  mulcmpblnq0  7252  mulcanenq0ec  7253  addclnq0  7259  nqpnq0nq  7261  nqnq0a  7262  nqnq0m  7263  nq0m0r  7264  nq0a0  7265  nnanq0  7266  distrnq0  7267  mulcomnq0  7268  addassnq0lemcl  7269  addassnq0  7270  nq02m  7273  prarloclemlt  7301  prarloclemn  7307