Theorem eldisjsim1

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

	Ref	Expression
Assertion	eldisjsim1	⊢ ( 𝑅 ∈ Disjs → Disj 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eldisjsdisj	⊢ ( 𝑅 ∈ Disjs → ( 𝑅 ∈ Disjs ↔ Disj 𝑅 ) )
2	1	ibi	⊢ ( 𝑅 ∈ Disjs → Disj 𝑅 )