Theorem elnn 7886

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Tr wtr 5212  ωcom 7875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-lim 6366  df-om 7876

This theorem is used by:  nnaordi  8620  nnmordi  8633  pssnn  9177  ssnnfi  9178  unfilem1  9290  unfilem2  9291  inf3lem5  9626  cantnflt  9666  cantnfp1lem3  9674  cantnflem1d  9682  cantnflem1  9683  cnfcomlem  9693  cnfcom  9694  ttrcltr  9710  ttrclselem2  9720  elhf2  9903  hfelhfOLD  9909  infpssrlem4  10377  axdc3lem2  10522  pwfseqlem3  10738  oldfi  28293  n0bday  28731  onltn0s  28737  bnj1098  35407  bnj517  35508  bnj594  35535  bnj1001  35582  bnj1118  35607  bnj1128  35613  bnj1145  35616  fineqvnttrclselem2  35773  fineqvnttrclselem3  35774  mh-inf3f1  37309