Theorem orddisj

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

	Ref	Expression
Assertion	orddisj	⊢ ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ordirr	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
2		disjsn	⊢ ( ( 𝐴 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ 𝐴 )
3	1 2	sylibr	⊢ ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ )