![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2oex | Structured version Visualization version GIF version |
Description: 2o is a set. (Contributed by BJ, 6-Apr-2019.) Remove dependency on ax-10 2138, ax-11 2155, ax-12 2172, ax-un 7725. (Proof shortened by Zhi Wang, 19-Sep-2024.) |
Ref | Expression |
---|---|
2oex | ⊢ 2o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df2o3 8474 | . 2 ⊢ 2o = {∅, 1o} | |
2 | prex 5433 | . 2 ⊢ {∅, 1o} ∈ V | |
3 | 1, 2 | eqeltri 2830 | 1 ⊢ 2o ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3475 ∅c0 4323 {cpr 4631 1oc1o 8459 2oc2o 8460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-dif 3952 df-un 3954 df-nul 4324 df-sn 4630 df-pr 4632 df-suc 6371 df-1o 8466 df-2o 8467 |
This theorem is referenced by: 2on 8480 snnen2o 9237 1sdom2 9240 setc2obas 18044 setc2ohom 18045 nogt01o 27199 nosupbday 27208 noetainflem1 27240 noetainflem2 27241 noetainflem4 27243 fmlaomn0 34381 goaln0 34384 goalrlem 34387 goalr 34388 fmlasucdisj 34390 satffunlem1lem1 34393 satffunlem2lem1 34395 ex-sategoelel12 34418 oenord1ex 42065 onno 42184 clsk1indlem1 42796 clsk1independent 42797 setc2othin 47676 |
Copyright terms: Public domain | W3C validator |