Theorem orddisj

Description: An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998)

	Ref	Expression
Assertion	orddisj	$$⊢\mathrm{Ord}A\to A\cap \left\{A\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
2		disjsn	$$⊢A\cap \left\{A\right\}=\varnothing \leftrightarrow \neg A\in A$$
3	1 2	sylibr	$$⊢\mathrm{Ord}A\to A\cap \left\{A\right\}=\varnothing$$