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 \in On \leftrightarrow suc A \in On$

Proof

Step	Hyp	Ref	Expression
1		ordsuc	$⊢ Ord A \leftrightarrow Ord suc A$
2		sucexb	$⊢ A \in V \leftrightarrow suc A \in V$
3	1 2	anbi12i	$⊢ (Ord A \land A \in V) \leftrightarrow (Ord suc A \land suc A \in V)$
4		elon2	$⊢ A \in On \leftrightarrow (Ord A \land A \in V)$
5		elon2	$⊢ suc A \in On \leftrightarrow (Ord suc A \land suc A \in V)$
6	3 4 5	3bitr4i	$⊢ A \in On \leftrightarrow suc A \in On$