Metamath Proof Explorer

Theorem orddisj

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

Ref Expression
Assertion orddisj 
|- ( Ord A -> ( A i^i { A } ) = (/) )

Proof

Step Hyp Ref Expression
1 ordirr 
 |-  ( Ord A -> -. A e. A )
2 disjsn 
 |-  ( ( A i^i { A } ) = (/) <-> -. A e. A )
3 1 2 sylibr 
 |-  ( Ord A -> ( A i^i { A } ) = (/) )