Theorem elnn 7833

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Tr wtr 5209  ωcom 7822

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-lim 6325  df-om 7823

This theorem is referenced by:  nnaordi  8559  nnmordi  8572  pssnn  9109  ssnnfi  9110  unfilem1  9230  unfilem2  9231  inf3lem5  9561  cantnflt  9601  cantnfp1lem3  9609  cantnflem1d  9617  cantnflem1  9618  cnfcomlem  9628  cnfcom  9629  ttrcltr  9645  ttrclselem2  9655  infpssrlem4  10235  axdc3lem2  10380  pwfseqlem3  10589  oldfi  27801  n0sbday  28220  onltn0s  28224  zs12bday  28319  bnj1098  34746  bnj517  34848  bnj594  34875  bnj1001  34922  bnj1118  34947  bnj1128  34953  bnj1145  34956  elhf2  36136  hfelhf  36142