Theorem oneli

Description: A member of an ordinal number is an ordinal number. Theorem 7M(a) of Enderton p. 192. (Contributed by NM, 11-Jun-1994)

	Ref	Expression
Hypothesis	on.1	⊢ 𝐴 ∈ On
Assertion	oneli	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		on.1	⊢ 𝐴 ∈ On
2		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ On )
3	1 2	mpan	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ On )