Theorem ordelss

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

	Ref	Expression
Assertion	ordelss	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ordtr	⊢ ( Ord 𝐴 → Tr 𝐴 )
2		trss	⊢ ( Tr 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴 ) )
3	2	imp	⊢ ( ( Tr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ⊆ 𝐴 )
4	1 3	sylan	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ⊆ 𝐴 )