Theorem eldisjsim2

Description: An element of the class of disjoint relations is an element of the class of relations. (Contributed by Peter Mazsa, 11-Feb-2026)

	Ref	Expression
Assertion	eldisjsim2	$$⊢R\in \mathrm{Disjs}\to R\in \mathrm{Rels}$$

Proof

Step	Hyp	Ref	Expression
1		elinel2	$$⊢R\in \left(\mathrm{Disjss}\cap \mathrm{Rels}\right)\to R\in \mathrm{Rels}$$
2		df-disjs	$$⊢\mathrm{Disjs}=\mathrm{Disjss}\cap \mathrm{Rels}$$
3	1 2	eleq2s	$$⊢R\in \mathrm{Disjs}\to R\in \mathrm{Rels}$$