This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )