Theorem 2oex 8471

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

Step	Hyp	Ref	Expression
1		df2o3 8467	. 2 ⊢ 2o = {∅, 1o}
2		prex 5411	. 2 ⊢ {∅, 1o} ∈ V
3	1, 2	eqeltri 2861	1 ⊢ 2o ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ∅c0 4286  {cpr 4593  1_oc1o 8452  2_oc2o 8453

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-sn 4592  df-pr 4594  df-suc 6370  df-1o 8459  df-2o 8460

This theorem is used by:  2on  8473  snnen2o  9212  1sdom2  9215  setc2obas  18173  setc2ohom  18174  degenmgmopdm  19034  degenmgm  19037  degenmgm2opdm  19038  degenmgm2nfun  19039  degenmgm2  19040  nogt01o  27911  nosupbday  27920  noetainflem1  27952  noetainflem2  27953  noetainflem4  27955  fmlaomn0  35919  goaln0  35922  goalrlem  35925  goalr  35926  fmlasucdisj  35928  satffunlem1lem1  35931  satffunlem2lem1  35933  ex-sategoelel12  35956  oenord1ex  44100  onnoxp  44217  clsk1indlem1  44829  clsk1independent  44830  nelsubc3  49906  setc2othin  50301  setc1onsubc  50437