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

Theorem elnn 7621
Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.)
Assertion
Ref Expression
elnn ((𝐴𝐵𝐵 ∈ ω) → 𝐴 ∈ ω)

Proof of Theorem elnn
StepHypRef Expression
1 ordom 7620 . 2 Ord ω
2 ordtr 6196 . 2 (Ord ω → Tr ω)
3 trel 5153 . 2 (Tr ω → ((𝐴𝐵𝐵 ∈ ω) → 𝐴 ∈ ω))
41, 2, 3mp2b 10 1 ((𝐴𝐵𝐵 ∈ ω) → 𝐴 ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2114  Tr wtr 5146  Ord word 6181  ωcom 7611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-11 2162  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306  ax-un 7491
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-tr 5147  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-we 5495  df-ord 6185  df-on 6186  df-lim 6187  df-om 7612
This theorem is referenced by:  nnaordi  8287  nnmordi  8300  pssnn  8779  ssnnfi  8780  ssnnfiOLD  8781  pssnnOLD  8827  unfilem1  8868  unfilem2  8869  inf3lem5  9180  cantnflt  9220  cantnfp1lem3  9228  cantnflem1d  9236  cantnflem1  9237  cnfcomlem  9247  cnfcom  9248  infpssrlem4  9818  axdc3lem2  9963  pwfseqlem3  10172  bnj1098  32346  bnj517  32448  bnj594  32475  bnj1001  32522  bnj1118  32547  bnj1128  32553  bnj1145  32556  elhf2  34132  hfelhf  34138
  Copyright terms: Public domain W3C validator