Theorem 2oex 8391

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8388	. 2 ⊢ 2o = {∅, 1o}
2		prex 5370	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2827	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ∅c0 4278  {cpr 4573  1_oc1o 8373  2_oc2o 8374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-nul 4279  df-sn 4572  df-pr 4574  df-suc 6307  df-1o 8380  df-2o 8381

This theorem is referenced by:  2on  8393  snnen2o  9124  1sdom2  9127  setc2obas  17996  setc2ohom  17997  nogt01o  27630  nosupbday  27639  noetainflem1  27671  noetainflem2  27672  noetainflem4  27674  fmlaomn0  35426  goaln0  35429  goalrlem  35432  goalr  35433  fmlasucdisj  35435  satffunlem1lem1  35438  satffunlem2lem1  35440  ex-sategoelel12  35463  oenord1ex  43348  onno  43466  clsk1indlem1  44078  clsk1independent  44079  nelsubc3  49103  setc2othin  49498  setc1onsubc  49634