Metamath Proof Explorer

Theorem disjrel

Description: Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021)

Ref Expression
Assertion disjrel 
|- ( Disj R -> Rel R )

Proof

Step Hyp Ref Expression
1 df-disjALTV 
 |-  ( Disj R <-> ( CnvRefRel ,~ `' R /\ Rel R ) )
2 1 simprbi 
 |-  ( Disj R -> Rel R )