Theorem pinn 7311

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 7306	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3263	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3189	. 2 ⊢ N ⊆ ω
4	3	sseli 3153	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2148   ∖ cdif 3128  ∅c0 3424  {csn 3594  ωcom 4591  Ncnpi 7274

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-dif 3133  df-in 3137  df-ss 3144  df-ni 7306

This theorem is referenced by:  pion  7312  piord  7313  elni2  7316  mulidpi  7320  ltsopi  7322  pitric  7323  pitri3or  7324  ltdcpi  7325  addclpi  7329  mulclpi  7330  addcompig  7331  addasspig  7332  mulcompig  7333  mulasspig  7334  distrpig  7335  addcanpig  7336  mulcanpig  7337  addnidpig  7338  ltexpi  7339  ltapig  7340  ltmpig  7341  nnppipi  7345  enqdc  7363  archnqq  7419  prarloclemarch2  7421  enq0enq  7433  enq0sym  7434  enq0ref  7435  enq0tr  7436  nqnq0pi  7440  nqnq0  7443  addcmpblnq0  7445  mulcmpblnq0  7446  mulcanenq0ec  7447  addclnq0  7453  nqpnq0nq  7455  nqnq0a  7456  nqnq0m  7457  nq0m0r  7458  nq0a0  7459  nnanq0  7460  distrnq0  7461  mulcomnq0  7462  addassnq0lemcl  7463  addassnq0  7464  nq02m  7467  prarloclemlt  7495  prarloclemn  7501