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	⊢ Disjs ⊆ Rels

Proof

Step	Hyp	Ref	Expression
1		eldisjsim2	⊢ ( 𝑟 ∈ Disjs → 𝑟 ∈ Rels )
2	1	ssriv	⊢ Disjs ⊆ Rels