Theorem pinn 7624

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 7619	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 3345	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3270	. 2 ⊢ N ⊆ ω
4	3	sseli 3234	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2203   ∖ cdif 3208  ∅c0 3508  {csn 3689  ωcom 4712  Ncnpi 7587

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-dif 3213  df-in 3217  df-ss 3224  df-ni 7619

This theorem is referenced by:  pion  7625  piord  7626  elni2  7629  mulidpi  7633  ltsopi  7635  pitric  7636  pitri3or  7637  ltdcpi  7638  addclpi  7642  mulclpi  7643  addcompig  7644  addasspig  7645  mulcompig  7646  mulasspig  7647  distrpig  7648  addcanpig  7649  mulcanpig  7650  addnidpig  7651  ltexpi  7652  ltapig  7653  ltmpig  7654  nnppipi  7658  enqdc  7676  archnqq  7732  prarloclemarch2  7734  enq0enq  7746  enq0sym  7747  enq0ref  7748  enq0tr  7749  nqnq0pi  7753  nqnq0  7756  addcmpblnq0  7758  mulcmpblnq0  7759  mulcanenq0ec  7760  addclnq0  7766  nqpnq0nq  7768  nqnq0a  7769  nqnq0m  7770  nq0m0r  7771  nq0a0  7772  nnanq0  7773  distrnq0  7774  mulcomnq0  7775  addassnq0lemcl  7776  addassnq0  7777  nq02m  7780  prarloclemlt  7808  prarloclemn  7814