Theorem detinidres

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

	Ref	Expression
Assertion	detinidres	$$⊢Disj\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)\leftrightarrow EqvRel\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjALTVinidres	$$⊢Disj\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)$$
2	1	detlem	$$⊢Disj\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)\leftrightarrow EqvRel\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)$$