Theorem 2oex 8161

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8159	. 2 ⊢ 2o = {∅, 1o}
2		prex 5309	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2830	1 ⊢ 2o ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3400  ∅c0 4221  {cpr 4528  1_oc1o 8137  2_oc2o 8138

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-dif 3856  df-un 3858  df-nul 4222  df-sn 4527  df-pr 4529  df-suc 6189  df-1o 8144  df-2o 8145

This theorem is referenced by:  setc2obas  17479  setc2ohom  17480  fmlaomn0  32936  goaln0  32939  goalrlem  32942  goalr  32943  fmlasucdisj  32945  satffunlem1lem1  32948  satffunlem2lem1  32950  ex-sategoelel12  32973  nogt01o  33555  nosupbday  33564  noetainflem1  33596  noetainflem2  33597  noetainflem4  33599  clsk1indlem1  41242  clsk1independent  41243  setc2othin  45849