Theorem pinn 7666

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

Assertion

Ref	Expression
pinn	⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Proof of Theorem pinn

Step	Hyp	Ref	Expression
1		df-ni 7661	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3355	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3280	. 2 ⊢ N ⊆ ω
4	3	sseli 3244	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2209   ∖ cdif 3217  ∅c0 3520  {csn 3705  ωcom 4732  Ncnpi 7629

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-dif 3222  df-in 3226  df-ss 3233  df-ni 7661

This theorem is referenced by:  pion  7667  piord  7668  elni2  7671  mulidpi  7675  ltsopi  7677  pitric  7678  pitri3or  7679  ltdcpi  7680  addclpi  7684  mulclpi  7685  addcompig  7686  addasspig  7687  mulcompig  7688  mulasspig  7689  distrpig  7690  addcanpig  7691  mulcanpig  7692  addnidpig  7693  ltexpi  7694  ltapig  7695  ltmpig  7696  nnppipi  7700  enqdc  7718  archnqq  7774  prarloclemarch2  7776  enq0enq  7788  enq0sym  7789  enq0ref  7790  enq0tr  7791  nqnq0pi  7795  nqnq0  7798  addcmpblnq0  7800  mulcmpblnq0  7801  mulcanenq0ec  7802  addclnq0  7808  nqpnq0nq  7810  nqnq0a  7811  nqnq0m  7812  nq0m0r  7813  nq0a0  7814  nnanq0  7815  distrnq0  7816  mulcomnq0  7817  addassnq0lemcl  7818  addassnq0  7819  nq02m  7822  prarloclemlt  7850  prarloclemn  7856