| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > on0eln0 | Structured version Visualization version GIF version | ||
| Description: An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.) |
| Ref | Expression |
|---|---|
| on0eln0 | ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eloni 6359 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
| 2 | ord0eln0 6406 | . 2 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 ∈ wcel 2145 ≠ wne 2960 ∅c0 4288 Ord word 6348 Oncon0 6349 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5250 ax-pr 5394 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-tr 5212 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-ord 6352 df-on 6353 |
| This theorem is referenced by: ondif1 8474 oe0lem 8486 oevn0 8488 oa00 8532 omord 8541 om00 8548 om00el 8549 omeulem1 8555 omeulem2 8556 oewordri 8566 oeordsuc 8568 oelim2 8569 oeoa 8571 oeoe 8573 oeeui 8576 omabs 8625 omxpenlem 9054 cantnff 9631 cantnfp1 9638 cantnflem1d 9645 cantnflem1 9646 cantnflem3 9648 cantnflem4 9649 cantnf 9650 cnfcomlem 9656 cnfcom3 9661 r1tskina 10755 onsucconni 36805 onint1 36817 frlmpwfi 43682 omge1 43881 omge2 43882 omlim2 43883 omord2lim 43884 omord2i 43885 dflim5 43913 tfsconcatb0 43928 tfsconcat0b 43930 oaun3lem1 43958 naddwordnexlem4 43985 omltoe 43990 |
| Copyright terms: Public domain | W3C validator |