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

Proof

Step Hyp Ref Expression
1 eldisjsdisj 
 |-  ( R e. Disjs -> ( R e. Disjs <-> Disj R ) )
2 1 ibi 
 |-  ( R e. Disjs -> Disj R )