Theorem 2oex 8461

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8457	. 2 ⊢ 2o = {∅, 1o}
2		prex 5409	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2859	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ∅c0 4286  {cpr 4591  1_oc1o 8442  2_oc2o 8443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4590  df-pr 4592  df-suc 6366  df-1o 8449  df-2o 8450

This theorem is referenced by:  2on  8463  snnen2o  9201  1sdom2  9204  setc2obas  18146  setc2ohom  18147  nogt01o  27860  nosupbday  27869  noetainflem1  27901  noetainflem2  27902  noetainflem4  27904  fmlaomn0  35882  goaln0  35885  goalrlem  35888  goalr  35889  fmlasucdisj  35891  satffunlem1lem1  35894  satffunlem2lem1  35896  ex-sategoelel12  35919  oenord1ex  44042  onnoxp  44159  clsk1indlem1  44771  clsk1independent  44772  nelsubc3  49849  setc2othin  50244  setc1onsubc  50380