![]() |
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 2139, ax-11 2155, ax-12 2175, ax-un 7754. (Proof shortened by Zhi Wang, 19-Sep-2024.) |
Ref | Expression |
---|---|
2oex | ⊢ 2o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df2o3 8513 | . 2 ⊢ 2o = {∅, 1o} | |
2 | prex 5443 | . 2 ⊢ {∅, 1o} ∈ V | |
3 | 1, 2 | eqeltri 2835 | 1 ⊢ 2o ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3478 ∅c0 4339 {cpr 4633 1oc1o 8498 2oc2o 8499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-dif 3966 df-un 3968 df-nul 4340 df-sn 4632 df-pr 4634 df-suc 6392 df-1o 8505 df-2o 8506 |
This theorem is referenced by: 2on 8519 snnen2o 9271 1sdom2 9274 setc2obas 18148 setc2ohom 18149 nogt01o 27756 nosupbday 27765 noetainflem1 27797 noetainflem2 27798 noetainflem4 27800 fmlaomn0 35375 goaln0 35378 goalrlem 35381 goalr 35382 fmlasucdisj 35384 satffunlem1lem1 35387 satffunlem2lem1 35389 ex-sategoelel12 35412 oenord1ex 43305 onno 43423 clsk1indlem1 44035 clsk1independent 44036 setc2othin 48857 |
Copyright terms: Public domain | W3C validator |