Theorem ordelss

Description: An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994)

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

Proof

Step	Hyp	Ref	Expression
1		ordtr	$$⊢\mathrm{Ord}A\to \mathrm{Tr}A$$
2		trss	$$⊢\mathrm{Tr}A\to \left(B\in A\to B\subseteq A\right)$$
3	2	imp	$$⊢\left(\mathrm{Tr}A\wedge B\in A\right)\to B\subseteq A$$
4	1 3	sylan	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to B\subseteq A$$