Theorem 2oex

Description: 2o is a set. (Contributed by BJ, 6-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		df-2o	|- 2o = suc 1o
2		1oex	|- 1o e. _V
3	2	sucex	|- suc 1o e. _V
4	1 3	eqeltri	|- 2o e. _V