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 6198 | . 2 ⊢ (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴)) | |
2 | df-on 6195 | . 2 ⊢ On = {𝑥 ∣ Ord 𝑥} | |
3 | 1, 2 | elab2g 3578 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∈ wcel 2112 Ord word 6190 Oncon0 6191 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-v 3400 df-in 3860 df-ss 3870 df-uni 4806 df-tr 5147 df-po 5453 df-so 5454 df-fr 5494 df-we 5496 df-ord 6194 df-on 6195 |
This theorem is referenced by: elon 6200 eloni 6201 elon2 6202 ordelon 6215 onin 6222 limelon 6254 ordsssuc2 6279 onprc 7540 ssonuni 7542 suceloni 7570 ordsuc 7571 oion 9130 hartogs 9138 card2on 9148 tskwe 9531 onssnum 9619 hsmexlem1 10005 ondomon 10142 1stcrestlem 22303 nosupno 33592 noinfno 33607 hfninf 34174 |
Copyright terms: Public domain | W3C validator |