Theorem idsymrel

Description: The identity relation is symmetric. (Contributed by AV, 19-Jun-2022)

	Ref	Expression
Assertion	idsymrel	$$⊢SymRel\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
2		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
3		dfsymrel4	$$⊢SymRel\mathrm{I}\leftrightarrow \left({\mathrm{I}}^{-1}=\mathrm{I}\wedge \mathrm{Rel}\mathrm{I}\right)$$
4	1 2 3	mpbir2an	$$⊢SymRel\mathrm{I}$$