Metamath Proof Explorer

Theorem 2oexOLD

Description: Obsolete version of 2oex as of 19-Sep-2024. (Contributed by BJ, 6-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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