Theorem elon2

Description: An ordinal number is an ordinal set. Part of Definition 1.2 of Schloeder p. 1. (Contributed by NM, 8-Feb-2004)

	Ref	Expression
Assertion	elon2	$$⊢A\in \mathrm{On}\leftrightarrow \left(\mathrm{Ord}A\wedge A\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \mathrm{On}\to A\in \mathrm{V}$$
2		elong	$$⊢A\in \mathrm{V}\to \left(A\in \mathrm{On}\leftrightarrow \mathrm{Ord}A\right)$$
3	1 2	biadanii	$$⊢A\in \mathrm{On}\leftrightarrow \left(A\in \mathrm{V}\wedge \mathrm{Ord}A\right)$$
4	3	biancomi	$$⊢A\in \mathrm{On}\leftrightarrow \left(\mathrm{Ord}A\wedge A\in \mathrm{V}\right)$$