Theorem 2oex 8399

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ∅c0 4284  {cpr 4579  1_oc1o 8381  2_oc2o 8382

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 5235  ax-nul 5245  ax-pr 5371

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 3438  df-dif 3906  df-un 3908  df-nul 4285  df-sn 4578  df-pr 4580  df-suc 6313  df-1o 8388  df-2o 8389

This theorem is referenced by:  2on  8401  snnen2o  9134  1sdom2  9137  setc2obas  18001  setc2ohom  18002  nogt01o  27606  nosupbday  27615  noetainflem1  27647  noetainflem2  27648  noetainflem4  27650  fmlaomn0  35363  goaln0  35366  goalrlem  35369  goalr  35370  fmlasucdisj  35372  satffunlem1lem1  35375  satffunlem2lem1  35377  ex-sategoelel12  35400  oenord1ex  43288  onno  43406  clsk1indlem1  44018  clsk1independent  44019  nelsubc3  49056  setc2othin  49451  setc1onsubc  49587