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 5226	. 2 ⊢ (Tr ω → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω))
3	1, 2	ax-mp 5	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364  df-lim 6365  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  10285  axdc3lem2  10430  pwfseqlem3  10640  oldfi  28107  n0bday  28545  onltn0s  28551  bnj1098  35172  bnj517  35273  bnj594  35300  bnj1001  35347  bnj1118  35372  bnj1128  35378  bnj1145  35381  fineqvnttrclselem2  35535  fineqvnttrclselem3  35536  elhf2  36667  hfelhf  36673