Theorem pinn 7241

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 7236	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3243	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3169	. 2 ⊢ N ⊆ ω
4	3	sseli 3133	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2135   ∖ cdif 3108  ∅c0 3404  {csn 3570  ωcom 4561  Ncnpi 7204

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 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-dif 3113  df-in 3117  df-ss 3124  df-ni 7236

This theorem is referenced by:  pion  7242  piord  7243  elni2  7246  mulidpi  7250  ltsopi  7252  pitric  7253  pitri3or  7254  ltdcpi  7255  addclpi  7259  mulclpi  7260  addcompig  7261  addasspig  7262  mulcompig  7263  mulasspig  7264  distrpig  7265  addcanpig  7266  mulcanpig  7267  addnidpig  7268  ltexpi  7269  ltapig  7270  ltmpig  7271  nnppipi  7275  enqdc  7293  archnqq  7349  prarloclemarch2  7351  enq0enq  7363  enq0sym  7364  enq0ref  7365  enq0tr  7366  nqnq0pi  7370  nqnq0  7373  addcmpblnq0  7375  mulcmpblnq0  7376  mulcanenq0ec  7377  addclnq0  7383  nqpnq0nq  7385  nqnq0a  7386  nqnq0m  7387  nq0m0r  7388  nq0a0  7389  nnanq0  7390  distrnq0  7391  mulcomnq0  7392  addassnq0lemcl  7393  addassnq0  7394  nq02m  7397  prarloclemlt  7425  prarloclemn  7431