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

Theorem pinn 9685
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 9679 . . 3 N = (ω ∖ {∅})
2 difss 3729 . . 3 (ω ∖ {∅}) ⊆ ω
31, 2eqsstri 3627 . 2 N ⊆ ω
43sseli 3591 1 (𝐴N𝐴 ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  cdif 3564  c0 3907  {csn 4168  ωcom 7050  Ncnpi 9651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-in 3574  df-ss 3581  df-ni 9679
This theorem is referenced by:  pion  9686  piord  9687  mulidpi  9693  addclpi  9699  mulclpi  9700  addcompi  9701  addasspi  9702  mulcompi  9703  mulasspi  9704  distrpi  9705  addcanpi  9706  mulcanpi  9707  addnidpi  9708  ltexpi  9709  ltapi  9710  ltmpi  9711  indpi  9714
  Copyright terms: Public domain W3C validator