Theorem pinn 7442

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 7437	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3303	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3229	. 2 ⊢ N ⊆ ω
4	3	sseli 3193	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2177   ∖ cdif 3167  ∅c0 3464  {csn 3638  ωcom 4646  Ncnpi 7405

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3172  df-in 3176  df-ss 3183  df-ni 7437

This theorem is referenced by:  pion  7443  piord  7444  elni2  7447  mulidpi  7451  ltsopi  7453  pitric  7454  pitri3or  7455  ltdcpi  7456  addclpi  7460  mulclpi  7461  addcompig  7462  addasspig  7463  mulcompig  7464  mulasspig  7465  distrpig  7466  addcanpig  7467  mulcanpig  7468  addnidpig  7469  ltexpi  7470  ltapig  7471  ltmpig  7472  nnppipi  7476  enqdc  7494  archnqq  7550  prarloclemarch2  7552  enq0enq  7564  enq0sym  7565  enq0ref  7566  enq0tr  7567  nqnq0pi  7571  nqnq0  7574  addcmpblnq0  7576  mulcmpblnq0  7577  mulcanenq0ec  7578  addclnq0  7584  nqpnq0nq  7586  nqnq0a  7587  nqnq0m  7588  nq0m0r  7589  nq0a0  7590  nnanq0  7591  distrnq0  7592  mulcomnq0  7593  addassnq0lemcl  7594  addassnq0  7595  nq02m  7598  prarloclemlt  7626  prarloclemn  7632