Metamath Proof Explorer


Theorem disjrel

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

Ref Expression
Assertion disjrel ( Disj 𝑅 → Rel 𝑅 )

Proof

Step Hyp Ref Expression
1 df-disjALTV ( Disj 𝑅 ↔ ( CnvRefRel ≀ 𝑅 ∧ Rel 𝑅 ) )
2 1 simprbi ( Disj 𝑅 → Rel 𝑅 )