Theorem 2oex 8422

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8419	. 2 ⊢ 2o = {∅, 1o}
2		prex 5387	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2824	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  {cpr 4587  1_oc1o 8404  2_oc2o 8405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-un 3916  df-nul 4293  df-sn 4586  df-pr 4588  df-suc 6326  df-1o 8411  df-2o 8412

This theorem is referenced by:  2on  8424  snnen2o  9161  1sdom2  9164  setc2obas  18032  setc2ohom  18033  nogt01o  27584  nosupbday  27593  noetainflem1  27625  noetainflem2  27626  noetainflem4  27628  fmlaomn0  35350  goaln0  35353  goalrlem  35356  goalr  35357  fmlasucdisj  35359  satffunlem1lem1  35362  satffunlem2lem1  35364  ex-sategoelel12  35387  oenord1ex  43277  onno  43395  clsk1indlem1  44007  clsk1independent  44008  nelsubc3  49033  setc2othin  49428  setc1onsubc  49564