Theorem eqvrelid

Description: The identity relation is an equivalence relation. (Contributed by Peter Mazsa, 15-Apr-2019) (Revised by Peter Mazsa, 31-Dec-2021)

	Ref	Expression
Assertion	eqvrelid	⊢ EqvRel I

Proof

Step	Hyp	Ref	Expression
1		disjALTVid	⊢ Disj I
2	1	disjimi	⊢ EqvRel ≀ I
3		cossid	⊢ ≀ I = I
4	3	eqvreleqi	⊢ ( EqvRel ≀ I ↔ EqvRel I )
5	2 4	mpbi	⊢ EqvRel I