Theorem detid

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

	Ref	Expression
Assertion	detid	$$⊢Disj\mathrm{I}\leftrightarrow EqvRel\wr \mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		disjALTVid	$$⊢Disj\mathrm{I}$$
2	1	detlem	$$⊢Disj\mathrm{I}\leftrightarrow EqvRel\wr \mathrm{I}$$