![]() |
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 7847 | . 2 ⊢ Tr ω | |
2 | trel 5267 | . 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 5258 ωcom 7838 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-opab 5204 df-tr 5259 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-ord 6356 df-on 6357 df-lim 6358 df-om 7839 |
This theorem is referenced by: nnaordi 8601 nnmordi 8614 pssnn 9151 ssnnfi 9152 ssnnfiOLD 9153 pssnnOLD 9248 unfilem1 9293 unfilem2 9294 inf3lem5 9609 cantnflt 9649 cantnfp1lem3 9657 cantnflem1d 9665 cantnflem1 9666 cnfcomlem 9676 cnfcom 9677 ttrcltr 9693 ttrclselem2 9703 infpssrlem4 10283 axdc3lem2 10428 pwfseqlem3 10637 bnj1098 33623 bnj517 33725 bnj594 33752 bnj1001 33799 bnj1118 33824 bnj1128 33830 bnj1145 33833 elhf2 34975 hfelhf 34981 |
Copyright terms: Public domain | W3C validator |