Theorem ordelon

Description: An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003)

	Ref	Expression
Assertion	ordelon	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to B\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		ordelord	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to \mathrm{Ord}B$$
2		elong	$$⊢B\in A\to \left(B\in \mathrm{On}\leftrightarrow \mathrm{Ord}B\right)$$
3	2	adantl	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to \left(B\in \mathrm{On}\leftrightarrow \mathrm{Ord}B\right)$$
4	1 3	mpbird	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to B\in \mathrm{On}$$