Theorem disjsssrels

Description: The class of disjoint relations is a subclass of the class of relations. (Contributed by Peter Mazsa, 11-Feb-2026)

	Ref	Expression
Assertion	disjsssrels	$$⊢\mathrm{Disjs}\subseteq \mathrm{Rels}$$

Proof

Step	Hyp	Ref	Expression
1		eldisjsim2	$$⊢r\in \mathrm{Disjs}\to r\in \mathrm{Rels}$$
2	1	ssriv	$$⊢\mathrm{Disjs}\subseteq \mathrm{Rels}$$