Metamath Proof Explorer


Theorem detidres

Description: The cosets by the restricted identity relation are in equivalence relation if and only if the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion detidres Disj I A EqvRel I A

Proof

Step Hyp Ref Expression
1 disjALTVidres Disj I A
2 1 detlem Disj I A EqvRel I A