![]() |
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 6078 | . 2 ⊢ (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴)) | |
2 | df-on 6075 | . 2 ⊢ On = {𝑥 ∣ Ord 𝑥} | |
3 | 1, 2 | elab2g 3608 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∈ wcel 2081 Ord word 6070 Oncon0 6071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-in 3870 df-ss 3878 df-uni 4750 df-tr 5069 df-po 5367 df-so 5368 df-fr 5407 df-we 5409 df-ord 6074 df-on 6075 |
This theorem is referenced by: elon 6080 eloni 6081 elon2 6082 ordelon 6095 onin 6102 limelon 6134 ordsssuc2 6159 onprc 7360 ssonuni 7362 suceloni 7389 ordsuc 7390 oion 8851 hartogs 8859 card2on 8869 tskwe 9230 onssnum 9317 hsmexlem1 9699 ondomon 9836 1stcrestlem 21749 nosupno 32818 hfninf 33262 |
Copyright terms: Public domain | W3C validator |