Theorem 2oex 8467

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ∅c0 4279  {cpr 4586  1_oc1o 8448  2_oc2o 8449

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-pr 4587  df-suc 6363  df-1o 8455  df-2o 8456

This theorem is used by:  2on  8469  snnen2o  9215  1sdom2  9218  setc2obas  18183  setc2ohom  18184  degenmgmopdm  19047  degenmgm  19050  degenmgm2opdm  19051  degenmgm2nfun  19052  degenmgm2  19053  nogt01o  27932  nosupbday  27941  noetainflem1  27973  noetainflem2  27974  noetainflem4  27976  fmlaomn0  35969  goaln0  35972  goalrlem  35975  goalr  35976  fmlasucdisj  35978  satffunlem1lem1  35981  satffunlem2lem1  35983  ex-sategoelel12  36006  oenord1ex  44156  onnoxp  44273  clsk1indlem1  44885  clsk1independent  44886  nelsubc3  49997  setc2othin  50392  setc1onsubc  50528