Theorem 2oex 8526

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8522	. 2 ⊢ 2o = {∅, 1o}
2		prex 5403	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2860	1 ⊢ 2o ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  {cpr 4590  1_oc1o 8507  2_oc2o 8508

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591  df-suc 6394  df-1o 8514  df-2o 8515

This theorem is used by:  2on  8528  snnen2o  9274  1sdom2  9277  setc2obas  18319  setc2ohom  18320  degenmgmopdm  19184  degenmgm  19187  degenmgm2opdm  19188  degenmgm2nfun  19189  degenmgm2  19190  nogt01o  28110  nosupbday  28119  noetainflem1  28151  noetainflem2  28152  noetainflem4  28154  fmlaomn0  36363  goaln0  36366  goalrlem  36369  goalr  36370  fmlasucdisj  36372  satffunlem1lem1  36375  satffunlem2lem1  36377  ex-sategoelel12  36400  oenord1ex  44578  onnoxp  44695  clsk1indlem1  45306  clsk1independent  45307  nelsubc3  50516  setc2othin  50932  setc1onsubc  51071  par2catid  51098  par2str  51100  parswapval  51107  parswapprop  51108  par2hom  51110  fuconuniqlem  51112  fuconuniqvalslem  51114