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	⊢ ( 𝑅 ∈ Disjs → 𝑅 ∈ Rels )

Proof

Step	Hyp	Ref	Expression
1		elinel2	⊢ ( 𝑅 ∈ ( Disjss ∩ Rels ) → 𝑅 ∈ Rels )
2		df-disjs	⊢ Disjs = ( Disjss ∩ Rels )
3	1 2	eleq2s	⊢ ( 𝑅 ∈ Disjs → 𝑅 ∈ Rels )