Theorem ord0

Description: The empty set is an ordinal class. Remark 1.5 of Schloeder p. 1. (Contributed by NM, 11-May-1994)

	Ref	Expression
Assertion	ord0	⊢ Ord ∅

Proof

Step	Hyp	Ref	Expression
1		tr0	⊢ Tr ∅
2		we0	⊢ E We ∅
3		df-ord	⊢ ( Ord ∅ ↔ ( Tr ∅ ∧ E We ∅ ) )
4	1 2 3	mpbir2an	⊢ Ord ∅