Theorem elnn 7898

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Tr wtr 5259  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-om 7888

This theorem is referenced by:  nnaordi  8656  nnmordi  8669  pssnn  9208  ssnnfi  9209  unfilem1  9343  unfilem2  9344  inf3lem5  9672  cantnflt  9712  cantnfp1lem3  9720  cantnflem1d  9728  cantnflem1  9729  cnfcomlem  9739  cnfcom  9740  ttrcltr  9756  ttrclselem2  9766  infpssrlem4  10346  axdc3lem2  10491  pwfseqlem3  10700  oldfi  27951  n0sbday  28354  pw2bday  28418  zs12bday  28424  bnj1098  34797  bnj517  34899  bnj594  34926  bnj1001  34973  bnj1118  34998  bnj1128  35004  bnj1145  35007  elhf2  36176  hfelhf  36182