Theorem elnn 7869

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

Step	Hyp	Ref	Expression
1		trom 7867	. 2 ⊢ Tr ω
2		trel 5227	. 2 ⊢ (Tr ω → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω))
3	1, 2	ax-mp 5	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  Tr wtr 5219  ωcom 7858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6361  df-on 6362  df-lim 6363  df-om 7859

This theorem is referenced by:  nnaordi  8600  nnmordi  8613  pssnn  9149  ssnnfi  9150  unfilem1  9261  unfilem2  9262  inf3lem5  9597  cantnflt  9637  cantnfp1lem3  9645  cantnflem1d  9653  cantnflem1  9654  cnfcomlem  9664  cnfcom  9665  ttrcltr  9681  ttrclselem2  9691  infpssrlem4  10286  axdc3lem2  10431  pwfseqlem3  10641  oldfi  28069  n0bday  28507  onltn0s  28513  bnj1098  35113  bnj517  35214  bnj594  35241  bnj1001  35288  bnj1118  35313  bnj1128  35319  bnj1145  35322  fineqvnttrclselem2  35454  fineqvnttrclselem3  35455  elhf2  36562  hfelhf  36568