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

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