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 ≀ I

Proof

Step	Hyp	Ref	Expression
1		disjALTVid	⊢ Disj I
2	1	disjimi	⊢ EqvRel ≀ I