Theorem elnn 7849

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Tr wtr 5258  ωcom 7838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-tr 5259  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-ord 6356  df-on 6357  df-lim 6358  df-om 7839

This theorem is referenced by:  nnaordi  8601  nnmordi  8614  pssnn  9151  ssnnfi  9152  ssnnfiOLD  9153  pssnnOLD  9248  unfilem1  9293  unfilem2  9294  inf3lem5  9609  cantnflt  9649  cantnfp1lem3  9657  cantnflem1d  9665  cantnflem1  9666  cnfcomlem  9676  cnfcom  9677  ttrcltr  9693  ttrclselem2  9703  infpssrlem4  10283  axdc3lem2  10428  pwfseqlem3  10637  bnj1098  33623  bnj517  33725  bnj594  33752  bnj1001  33799  bnj1118  33824  bnj1128  33830  bnj1145  33833  elhf2  34975  hfelhf  34981