ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elnn GIF version

Theorem elnn 4607
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
StepHypRef Expression
1 elomssom 4606 . 2 (𝐵 ∈ ω → 𝐵 ⊆ ω)
2 ssel2 3152 . . 3 ((𝐵 ⊆ ω ∧ 𝐴𝐵) → 𝐴 ∈ ω)
32ancoms 268 . 2 ((𝐴𝐵𝐵 ⊆ ω) → 𝐴 ∈ ω)
41, 3sylan2 286 1 ((𝐴𝐵𝐵 ∈ ω) → 𝐴 ∈ ω)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wss 3131  ωcom 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-uni 3812  df-int 3847  df-suc 4373  df-iom 4592
This theorem is referenced by:  ordom  4608  peano2b  4616  nntr2  6506  nndifsnid  6510  nnaordi  6511  nnmordi  6519  fidceq  6871  nnwetri  6917  enumctlemm  7115  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  2onetap  7256  2omotaplemap  7258  ennnfonelemdm  12423  ennnfonelemnn0  12425  xpscf  12771  nnti  14829  nninfsellemdc  14844  nninfsellemeq  14848  nninfsellemeqinf  14850
  Copyright terms: Public domain W3C validator