Metamath Proof Explorer

Theorem 0trrel

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

Ref Expression
Assertion 0trrel ( ∅ ∘ ∅ ) ⊆ ∅

Proof

Step Hyp Ref Expression
1 co01 ⊢ ( ∅ ∘ ∅ ) = ∅
2 1 eqimssi ⊢ ( ∅ ∘ ∅ ) ⊆ ∅