Theorem eqvrelcossid

Description: The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024)

	Ref	Expression
Assertion	eqvrelcossid	$$⊢EqvRel\wr \mathrm{I}$$

Proof

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