Theorem 2oex 8418

Description: 2_o is a set. (Contributed by BJ, 6-Apr-2019.) Remove dependency on ax-10 2147, ax-11 2163, ax-12 2185, ax-un 7690. (Proof shortened by Zhi Wang, 19-Sep-2024.)

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8415	. 2 ⊢ 2o = {∅, 1o}
2		prex 5384	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2833	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  {cpr 4584  1_oc1o 8400  2_oc2o 8401

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288  df-sn 4583  df-pr 4585  df-suc 6331  df-1o 8407  df-2o 8408

This theorem is referenced by:  2on  8420  snnen2o  9157  1sdom2  9160  setc2obas  18030  setc2ohom  18031  nogt01o  27676  nosupbday  27685  noetainflem1  27717  noetainflem2  27718  noetainflem4  27720  fmlaomn0  35606  goaln0  35609  goalrlem  35612  goalr  35613  fmlasucdisj  35615  satffunlem1lem1  35618  satffunlem2lem1  35620  ex-sategoelel12  35643  oenord1ex  43672  onnoxp  43789  clsk1indlem1  44401  clsk1independent  44402  nelsubc3  49430  setc2othin  49825  setc1onsubc  49961