Metamath Proof Explorer

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 e. Disjs -> R e. Rels )

Proof

Step Hyp Ref Expression
1 elinel2 
 |-  ( R e. ( Disjss i^i Rels ) -> R e. Rels )
2 df-disjs 
 |-  Disjs = ( Disjss i^i Rels )
3 1 2 eleq2s 
 |-  ( R e. Disjs -> R e. Rels )