Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elnn | Structured version Visualization version GIF version |
Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
Ref | Expression |
---|---|
elnn | ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trom 7721 | . 2 ⊢ Tr ω | |
2 | trel 5198 | . 2 ⊢ (Tr ω → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 Tr wtr 5191 ωcom 7712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-ral 3069 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-tr 5192 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-ord 6269 df-on 6270 df-lim 6271 df-om 7713 |
This theorem is referenced by: nnaordi 8449 nnmordi 8462 pssnn 8951 ssnnfi 8952 ssnnfiOLD 8953 pssnnOLD 9040 unfilem1 9078 unfilem2 9079 inf3lem5 9390 cantnflt 9430 cantnfp1lem3 9438 cantnflem1d 9446 cantnflem1 9447 cnfcomlem 9457 cnfcom 9458 ttrcltr 9474 ttrclselem2 9484 infpssrlem4 10062 axdc3lem2 10207 pwfseqlem3 10416 bnj1098 32763 bnj517 32865 bnj594 32892 bnj1001 32939 bnj1118 32964 bnj1128 32970 bnj1145 32973 elhf2 34477 hfelhf 34483 |
Copyright terms: Public domain | W3C validator |