Theorem elnn 7828

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

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

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327  df-lim 6328  df-om 7818

This theorem is referenced by:  nnaordi  8554  nnmordi  8567  pssnn  9103  ssnnfi  9104  unfilem1  9215  unfilem2  9216  inf3lem5  9553  cantnflt  9593  cantnfp1lem3  9601  cantnflem1d  9609  cantnflem1  9610  cnfcomlem  9620  cnfcom  9621  ttrcltr  9637  ttrclselem2  9647  infpssrlem4  10228  axdc3lem2  10373  pwfseqlem3  10583  oldfi  27906  n0bday  28344  onltn0s  28350  bnj1098  34926  bnj517  35027  bnj594  35054  bnj1001  35101  bnj1118  35126  bnj1128  35132  bnj1145  35135  fineqvnttrclselem2  35266  fineqvnttrclselem3  35267  elhf2  36357  hfelhf  36363