Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elong | Structured version Visualization version GIF version |
Description: An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
Ref | Expression |
---|---|
elong | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordeq 5647 | . 2 ⊢ (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴)) | |
2 | df-on 5644 | . 2 ⊢ On = {𝑥 ∣ Ord 𝑥} | |
3 | 1, 2 | elab2g 3322 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∈ wcel 1977 Ord word 5639 Oncon0 5640 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-v 3175 df-in 3547 df-ss 3554 df-uni 4373 df-tr 4681 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-ord 5643 df-on 5644 |
This theorem is referenced by: elon 5649 eloni 5650 elon2 5651 ordelon 5664 onin 5671 limelon 5705 ordsssuc2 5731 onprc 6876 ssonuni 6878 suceloni 6905 ordsuc 6906 oion 8324 hartogs 8332 card2on 8342 tskwe 8659 onssnum 8746 hsmexlem1 9131 ondomon 9264 1stcrestlem 21065 hfninf 31463 |
Copyright terms: Public domain | W3C validator |