Theorem 2oex

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

	Ref	Expression
Assertion	2oex	$$⊢2_{𝑜}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
2		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
3	2	sucex	$$⊢\mathrm{suc}{1}_{𝑜}\in \mathrm{V}$$
4	1 3	eqeltri	$$⊢2_{𝑜}\in \mathrm{V}$$