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 -1 Rel R
2 1 simprbi Disj R Rel R