Theorem 2oex 8495

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

Assertion

Ref	Expression
2oex	⊢ 2o ∈ V

Proof of Theorem 2oex

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ∅c0 4277  {cpr 4586  1_oc1o 8476  2_oc2o 8477

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4046  df-un 4150  df-nul 4278  df-sn 4585  df-pr 4587  df-suc 6371  df-1o 8483  df-2o 8484

This theorem is used by:  2on  8497  snnen2o  9243  1sdom2  9246  setc2obas  18278  setc2ohom  18279  degenmgmopdm  19143  degenmgm  19146  degenmgm2opdm  19147  degenmgm2nfun  19148  degenmgm2  19149  nogt01o  28062  nosupbday  28071  noetainflem1  28103  noetainflem2  28104  noetainflem4  28106  fmlaomn0  36245  goaln0  36248  goalrlem  36251  goalr  36252  fmlasucdisj  36254  satffunlem1lem1  36257  satffunlem2lem1  36259  ex-sategoelel12  36282  oenord1ex  44426  onnoxp  44543  clsk1indlem1  45154  clsk1independent  45155  nelsubc3  50293  setc2othin  50709  setc1onsubc  50848  par2catid  50875  par2str  50877  parswapval  50884  parswapprop  50885  par2hom  50887  fuconuniqlem  50889  fuconuniqvalslem  50891