Theorem 2oex 8533

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8530	. 2 ⊢ 2o = {∅, 1o}
2		prex 5452	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2840	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  {cpr 4650  1_oc1o 8515  2_oc2o 8516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-pr 4651  df-suc 6401  df-1o 8522  df-2o 8523

This theorem is referenced by:  2on  8536  snnen2o  9300  1sdom2  9303  setc2obas  18161  setc2ohom  18162  nogt01o  27759  nosupbday  27768  noetainflem1  27800  noetainflem2  27801  noetainflem4  27803  fmlaomn0  35358  goaln0  35361  goalrlem  35364  goalr  35365  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  ex-sategoelel12  35395  oenord1ex  43277  onno  43395  clsk1indlem1  44007  clsk1independent  44008  setc2othin  48723