Theorem onsssuc

Description: A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995)

	Ref	Expression
Assertion	onsssuc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
2		ordsssuc	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )