![]() |
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 2137, ax-11 2154, ax-12 2171, ax-un 7724. (Proof shortened by Zhi Wang, 19-Sep-2024.) |
Ref | Expression |
---|---|
2oex | ⊢ 2o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df2o3 8473 | . 2 ⊢ 2o = {∅, 1o} | |
2 | prex 5432 | . 2 ⊢ {∅, 1o} ∈ V | |
3 | 1, 2 | eqeltri 2829 | 1 ⊢ 2o ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3474 ∅c0 4322 {cpr 4630 1oc1o 8458 2oc2o 8459 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-dif 3951 df-un 3953 df-nul 4323 df-sn 4629 df-pr 4631 df-suc 6370 df-1o 8465 df-2o 8466 |
This theorem is referenced by: 2on 8479 snnen2o 9236 1sdom2 9239 setc2obas 18043 setc2ohom 18044 nogt01o 27196 nosupbday 27205 noetainflem1 27237 noetainflem2 27238 noetainflem4 27240 fmlaomn0 34376 goaln0 34379 goalrlem 34382 goalr 34383 fmlasucdisj 34385 satffunlem1lem1 34388 satffunlem2lem1 34390 ex-sategoelel12 34413 oenord1ex 42055 onno 42174 clsk1indlem1 42786 clsk1independent 42787 setc2othin 47666 |
Copyright terms: Public domain | W3C validator |