Theorem onelss

Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	onelss	$$⊢A\in \mathrm{On}\to \left(B\in A\to B\subseteq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		ordelss	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to B\subseteq A$$
3	2	ex	$$⊢\mathrm{Ord}A\to \left(B\in A\to B\subseteq A\right)$$
4	1 3	syl	$$⊢A\in \mathrm{On}\to \left(B\in A\to B\subseteq A\right)$$