Theorem elnn 7816

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Tr wtr 5202  ωcom 7805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318  df-lim 6319  df-om 7806

This theorem is referenced by:  nnaordi  8542  nnmordi  8555  pssnn  9089  ssnnfi  9090  unfilem1  9200  unfilem2  9201  inf3lem5  9533  cantnflt  9573  cantnfp1lem3  9581  cantnflem1d  9589  cantnflem1  9590  cnfcomlem  9600  cnfcom  9601  ttrcltr  9617  ttrclselem2  9627  infpssrlem4  10208  axdc3lem2  10353  pwfseqlem3  10562  oldfi  27879  n0sbday  28300  onltn0s  28304  zs12bday  28414  bnj1098  34867  bnj517  34969  bnj594  34996  bnj1001  35043  bnj1118  35068  bnj1128  35074  bnj1145  35077  fineqvnttrclselem2  35214  fineqvnttrclselem3  35215  elhf2  36291  hfelhf  36297