Theorem pinn 7369

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 7364	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3285	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3211	. 2 ⊢ N ⊆ ω
4	3	sseli 3175	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2164   ∖ cdif 3150  ∅c0 3446  {csn 3618  ωcom 4622  Ncnpi 7332

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3155  df-in 3159  df-ss 3166  df-ni 7364

This theorem is referenced by:  pion  7370  piord  7371  elni2  7374  mulidpi  7378  ltsopi  7380  pitric  7381  pitri3or  7382  ltdcpi  7383  addclpi  7387  mulclpi  7388  addcompig  7389  addasspig  7390  mulcompig  7391  mulasspig  7392  distrpig  7393  addcanpig  7394  mulcanpig  7395  addnidpig  7396  ltexpi  7397  ltapig  7398  ltmpig  7399  nnppipi  7403  enqdc  7421  archnqq  7477  prarloclemarch2  7479  enq0enq  7491  enq0sym  7492  enq0ref  7493  enq0tr  7494  nqnq0pi  7498  nqnq0  7501  addcmpblnq0  7503  mulcmpblnq0  7504  mulcanenq0ec  7505  addclnq0  7511  nqpnq0nq  7513  nqnq0a  7514  nqnq0m  7515  nq0m0r  7516  nq0a0  7517  nnanq0  7518  distrnq0  7519  mulcomnq0  7520  addassnq0lemcl  7521  addassnq0  7522  nq02m  7525  prarloclemlt  7553  prarloclemn  7559