This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onsucb

Description: A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc . (Contributed by NM, 9-Sep-2003)

Ref Expression
Assertion onsucb ⊢ 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