Theorem 2oex 8406

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8403	. 2 ⊢ 2o = {∅, 1o}
2		prex 5367	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2835	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  {cpr 4557  1_oc1o 8388  2_oc2o 8389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-un 3888  df-nul 4262  df-sn 4556  df-pr 4558  df-suc 6316  df-1o 8395  df-2o 8396

This theorem is referenced by:  2on  8408  snnen2o  9145  1sdom2  9148  setc2obas  18052  setc2ohom  18053  nogt01o  27678  nosupbday  27687  noetainflem1  27719  noetainflem2  27720  noetainflem4  27722  fmlaomn0  35618  goaln0  35621  goalrlem  35624  goalr  35625  fmlasucdisj  35627  satffunlem1lem1  35630  satffunlem2lem1  35632  ex-sategoelel12  35655  oenord1ex  43760  onnoxp  43877  clsk1indlem1  44489  clsk1independent  44490  nelsubc3  49561  setc2othin  49956  setc1onsubc  50092