Theorem 2oex 8409

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 7682. (Proof shortened by Zhi Wang, 19-Sep-2024.)

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  {cpr 4570  1_oc1o 8391  2_oc2o 8392

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 5231  ax-pr 5370

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 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-pr 4571  df-suc 6323  df-1o 8398  df-2o 8399

This theorem is referenced by:  2on  8411  snnen2o  9148  1sdom2  9151  setc2obas  18052  setc2ohom  18053  nogt01o  27674  nosupbday  27683  noetainflem1  27715  noetainflem2  27716  noetainflem4  27718  fmlaomn0  35588  goaln0  35591  goalrlem  35594  goalr  35595  fmlasucdisj  35597  satffunlem1lem1  35600  satffunlem2lem1  35602  ex-sategoelel12  35625  oenord1ex  43761  onnoxp  43878  clsk1indlem1  44490  clsk1independent  44491  nelsubc3  49558  setc2othin  49953  setc1onsubc  50089