Theorem elnn 7888

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Tr wtr 5211  ωcom 7877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367  df-om 7878

This theorem is used by:  nnaordi  8627  nnmordi  8640  pssnn  9184  ssnnfi  9185  unfilem1  9297  unfilem2  9298  inf3lem5  9633  cantnflt  9673  cantnfp1lem3  9681  cantnflem1d  9689  cantnflem1  9690  cnfcomlem  9700  cnfcom  9701  ttrcltr  9717  ttrclselem2  9727  elhf2  9910  hfelhfOLD  9916  infpssrlem4  10384  axdc3lem2  10529  pwfseqlem3  10745  oldfi  28300  n0bday  28738  onltn0s  28744  bnj1098  35456  bnj517  35557  bnj594  35584  bnj1001  35631  bnj1118  35656  bnj1128  35662  bnj1145  35665  fineqvnttrclselem2  35832  fineqvnttrclselem3  35833  mh-inf3f1  37371