Metamath Proof Explorer

Theorem eldisjsim1

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

Ref Expression
Assertion eldisjsim1 ⊢ R ∈ Disjs → Disj R

Proof

Step Hyp Ref Expression
1 eldisjsdisj ⊢ R ∈ Disjs → R ∈ Disjs ↔ Disj R
2 1 ibi ⊢ R ∈ Disjs → Disj R