Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pinn Structured version   Visualization version   GIF version

Theorem pinn 9579
 Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
Assertion
Ref Expression
pinn (𝐴N𝐴 ∈ ω)

Proof of Theorem pinn
StepHypRef Expression
1 df-ni 9573 . . 3 N = (ω ∖ {∅})
2 difss 3699 . . 3 (ω ∖ {∅}) ⊆ ω
31, 2eqsstri 3598 . 2 N ⊆ ω
43sseli 3564 1 (𝐴N𝐴 ∈ ω)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1977   ∖ cdif 3537  ∅c0 3874  {csn 4125  ωcom 6957  Ncnpi 9545 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-ni 9573 This theorem is referenced by:  pion  9580  piord  9581  mulidpi  9587  addclpi  9593  mulclpi  9594  addcompi  9595  addasspi  9596  mulcompi  9597  mulasspi  9598  distrpi  9599  addcanpi  9600  mulcanpi  9601  addnidpi  9602  ltexpi  9603  ltapi  9604  ltmpi  9605  indpi  9608
 Copyright terms: Public domain W3C validator