Theorem 2oex

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

	Ref	Expression
Assertion	2oex	⊢ 2o ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-2o	⊢ 2o = suc 1o
2		1oex	⊢ 1o ∈ V
3	2	sucex	⊢ suc 1o ∈ V
4	1 3	eqeltri	⊢ 2o ∈ V