Metamath Proof Explorer

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 C_ Rels

Proof

Step Hyp Ref Expression
1 eldisjsim2 
 |-  ( r e. Disjs -> r e. Rels )
2 1 ssriv 
 |-  Disjs C_ Rels