| 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 2141, ax-11 2157, ax-12 2177, ax-un 7755. (Proof shortened by Zhi Wang, 19-Sep-2024.) |
| Ref | Expression |
|---|---|
| 2oex | ⊢ 2o ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df2o3 8514 | . 2 ⊢ 2o = {∅, 1o} | |
| 2 | prex 5437 | . 2 ⊢ {∅, 1o} ∈ V | |
| 3 | 1, 2 | eqeltri 2837 | 1 ⊢ 2o ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∅c0 4333 {cpr 4628 1oc1o 8499 2oc2o 8500 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-un 3956 df-nul 4334 df-sn 4627 df-pr 4629 df-suc 6390 df-1o 8506 df-2o 8507 |
| This theorem is referenced by: 2on 8520 snnen2o 9273 1sdom2 9276 setc2obas 18139 setc2ohom 18140 nogt01o 27741 nosupbday 27750 noetainflem1 27782 noetainflem2 27783 noetainflem4 27785 fmlaomn0 35395 goaln0 35398 goalrlem 35401 goalr 35402 fmlasucdisj 35404 satffunlem1lem1 35407 satffunlem2lem1 35409 ex-sategoelel12 35432 oenord1ex 43328 onno 43446 clsk1indlem1 44058 clsk1independent 44059 setc2othin 49113 |
| Copyright terms: Public domain | W3C validator |