Metamath Proof Explorer

Theorem sucelon

Description: The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003)

Ref Expression
Assertion sucelon ⊢ A ∈ On ↔ suc ⁡ A ∈ On

Proof

Step Hyp Ref Expression
1 ordsuc ⊢ Ord ⁡ A ↔ Ord ⁡ suc ⁡ A
2 sucexb ⊢ A ∈ V ↔ suc ⁡ A ∈ V
3 1 2 anbi12i ⊢ Ord ⁡ A ∧ A ∈ V ↔ Ord ⁡ suc ⁡ A ∧ suc ⁡ A ∈ V
4 elon2 ⊢ A ∈ On ↔ Ord ⁡ A ∧ A ∈ V
5 elon2 ⊢ suc ⁡ A ∈ On ↔ Ord ⁡ suc ⁡ A ∧ suc ⁡ A ∈ V
6 3 4 5 3bitr4i ⊢ A ∈ On ↔ suc ⁡ A ∈ On