Metamath Proof Explorer

Theorem 2oex

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

Ref Expression
Assertion 2oex 
|- 2o e. _V

Proof

Step Hyp Ref Expression
1 df2o3 
 |-  2o = { (/) , 1o }
2 prex 
 |-  { (/) , 1o } e. _V
3 1 2 eqeltri 
 |-  2o e. _V