Theorem elnn 7892

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 7890	. 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 7881

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 5391

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 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369  df-lim 6370  df-om 7882

This theorem is used by:  nnaordi  8634  nnmordi  8647  pssnn  9191  ssnnfi  9192  unfilem1  9304  unfilem2  9305  inf3lem5  9640  cantnflt  9680  cantnfp1lem3  9688  cantnflem1d  9696  cantnflem1  9697  cnfcomlem  9707  cnfcom  9708  ttrcltr  9724  ttrclselem2  9734  elhf2  9917  hfelhfOLD  9923  infpssrlem4  10391  axdc3lem2  10536  pwfseqlem3  10752  oldfi  28309  n0bday  28747  onltn0s  28753  bnj1098  35464  bnj517  35565  bnj594  35592  bnj1001  35639  bnj1118  35664  bnj1128  35670  bnj1145  35673  fineqvnttrclselem2  35850  fineqvnttrclselem3  35851  mh-inf3f1  37425