Theorem pinn 7519

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 7514	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3331	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3257	. 2 ⊢ N ⊆ ω
4	3	sseli 3221	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2200   ∖ cdif 3195  ∅c0 3492  {csn 3667  ωcom 4686  Ncnpi 7482

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-dif 3200  df-in 3204  df-ss 3211  df-ni 7514

This theorem is referenced by:  pion  7520  piord  7521  elni2  7524  mulidpi  7528  ltsopi  7530  pitric  7531  pitri3or  7532  ltdcpi  7533  addclpi  7537  mulclpi  7538  addcompig  7539  addasspig  7540  mulcompig  7541  mulasspig  7542  distrpig  7543  addcanpig  7544  mulcanpig  7545  addnidpig  7546  ltexpi  7547  ltapig  7548  ltmpig  7549  nnppipi  7553  enqdc  7571  archnqq  7627  prarloclemarch2  7629  enq0enq  7641  enq0sym  7642  enq0ref  7643  enq0tr  7644  nqnq0pi  7648  nqnq0  7651  addcmpblnq0  7653  mulcmpblnq0  7654  mulcanenq0ec  7655  addclnq0  7661  nqpnq0nq  7663  nqnq0a  7664  nqnq0m  7665  nq0m0r  7666  nq0a0  7667  nnanq0  7668  distrnq0  7669  mulcomnq0  7670  addassnq0lemcl  7671  addassnq0  7672  nq02m  7675  prarloclemlt  7703  prarloclemn  7709