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 )