Theorem 0trrel

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

	Ref	Expression
Assertion	0trrel	$$⊢\varnothing \circ \varnothing \subseteq \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		co01	$$⊢\varnothing \circ \varnothing =\varnothing$$
2	1	eqimssi	$$⊢\varnothing \circ \varnothing \subseteq \varnothing$$