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\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		disjALTVid	$$⊢Disj\mathrm{I}$$
2	1	disjimi	$$⊢EqvRel\wr \mathrm{I}$$
3		cossid	$$⊢\wr \mathrm{I}=\mathrm{I}$$
4	3	eqvreleqi	$$⊢EqvRel\wr \mathrm{I}\leftrightarrow EqvRel\mathrm{I}$$
5	2 4	mpbi	$$⊢EqvRel\mathrm{I}$$