Theorem 0elsuc

Description: The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995)

	Ref	Expression
Assertion	0elsuc	⊢ ( Ord 𝐴 → ∅ ∈ suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ordsuc	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
2		nsuceq0	⊢ suc 𝐴 ≠ ∅
3		ord0eln0	⊢ ( Ord suc 𝐴 → ( ∅ ∈ suc 𝐴 ↔ suc 𝐴 ≠ ∅ ) )
4	2 3	mpbiri	⊢ ( Ord suc 𝐴 → ∅ ∈ suc 𝐴 )
5	1 4	sylbi	⊢ ( Ord 𝐴 → ∅ ∈ suc 𝐴 )