Metamath Proof Explorer

Theorem 0trrel

Description: The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion 0trrel 
|- ( (/) o. (/) ) C_ (/)

Proof

Step Hyp Ref Expression
1 co01 
 |-  ( (/) o. (/) ) = (/)
2 1 eqimssi 
 |-  ( (/) o. (/) ) C_ (/)