Metamath Proof Explorer

Theorem onsssuc

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

Ref Expression
Assertion onsssuc ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B

Proof

Step Hyp Ref Expression
1 eloni ⊢ B ∈ On → Ord ⁡ B
2 ordsssuc ⊢ A ∈ On ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ suc ⁡ B
3 1 2 sylan2 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B