Theorem 2oex 8416

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8413	. 2 ⊢ 2o = {∅, 1o}
2		prex 5380	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2832	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ∅c0 4273  {cpr 4569  1_oc1o 8398  2_oc2o 8399

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-sn 4568  df-pr 4570  df-suc 6329  df-1o 8405  df-2o 8406

This theorem is referenced by:  2on  8418  snnen2o  9155  1sdom2  9158  setc2obas  18061  setc2ohom  18062  nogt01o  27660  nosupbday  27669  noetainflem1  27701  noetainflem2  27702  noetainflem4  27704  fmlaomn0  35572  goaln0  35575  goalrlem  35578  goalr  35579  fmlasucdisj  35581  satffunlem1lem1  35584  satffunlem2lem1  35586  ex-sategoelel12  35609  oenord1ex  43743  onnoxp  43860  clsk1indlem1  44472  clsk1independent  44473  nelsubc3  49546  setc2othin  49941  setc1onsubc  50077