Metamath Proof Explorer

Theorem disjimi

Description: Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021)

Ref Expression
Hypothesis disjimi.1 
|- Disj R
Assertion disjimi 
|- EqvRel ,~ R

Proof

Step Hyp Ref Expression
1 disjimi.1 
 |-  Disj R
2 disjim 
 |-  ( Disj R -> EqvRel ,~ R )
3 1 2 ax-mp 
 |-  EqvRel ,~ R