Theorem pinn 7059

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 7054	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3166	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3093	. 2 ⊢ N ⊆ ω
4	3	sseli 3057	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 1461   ∖ cdif 3032  ∅c0 3327  {csn 3491  ωcom 4462  Ncnpi 7022

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-dif 3037  df-in 3041  df-ss 3048  df-ni 7054

This theorem is referenced by:  pion  7060  piord  7061  elni2  7064  mulidpi  7068  ltsopi  7070  pitric  7071  pitri3or  7072  ltdcpi  7073  addclpi  7077  mulclpi  7078  addcompig  7079  addasspig  7080  mulcompig  7081  mulasspig  7082  distrpig  7083  addcanpig  7084  mulcanpig  7085  addnidpig  7086  ltexpi  7087  ltapig  7088  ltmpig  7089  nnppipi  7093  enqdc  7111  archnqq  7167  prarloclemarch2  7169  enq0enq  7181  enq0sym  7182  enq0ref  7183  enq0tr  7184  nqnq0pi  7188  nqnq0  7191  addcmpblnq0  7193  mulcmpblnq0  7194  mulcanenq0ec  7195  addclnq0  7201  nqpnq0nq  7203  nqnq0a  7204  nqnq0m  7205  nq0m0r  7206  nq0a0  7207  nnanq0  7208  distrnq0  7209  mulcomnq0  7210  addassnq0lemcl  7211  addassnq0  7212  nq02m  7215  prarloclemlt  7243  prarloclemn  7249