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	⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )

Proof

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