Theorem elnn 7821

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Tr wtr 5193  ωcom 7810

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-om 7811

This theorem is referenced by:  nnaordi  8547  nnmordi  8560  pssnn  9096  ssnnfi  9097  unfilem1  9208  unfilem2  9209  inf3lem5  9544  cantnflt  9584  cantnfp1lem3  9592  cantnflem1d  9600  cantnflem1  9601  cnfcomlem  9611  cnfcom  9612  ttrcltr  9628  ttrclselem2  9638  infpssrlem4  10219  axdc3lem2  10364  pwfseqlem3  10574  oldfi  27920  n0bday  28358  onltn0s  28364  bnj1098  34942  bnj517  35043  bnj594  35070  bnj1001  35117  bnj1118  35142  bnj1128  35148  bnj1145  35151  fineqvnttrclselem2  35282  fineqvnttrclselem3  35283  elhf2  36373  hfelhf  36379