Theorem ercnv

Description: The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Assertion	ercnv	$$⊢R\mathrm{Er}A\to R^{-1}=R$$

Proof

Step	Hyp	Ref	Expression
1		errel	$$⊢R\mathrm{Er}A\to \mathrm{Rel}R$$
2		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
3		id	$$⊢R\mathrm{Er}A\to R\mathrm{Er}A$$
4	3	ersymb	$$⊢R\mathrm{Er}A\to \left(yRx\leftrightarrow xRy\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6		vex	$$⊢y\in \mathrm{V}$$
7	5 6	brcnv	$$⊢x{R}^{-1}y\leftrightarrow yRx$$
8		df-br	$$⊢x{R}^{-1}y\leftrightarrow ⟨x,y⟩\in R^{-1}$$
9	7 8	bitr3i	$$⊢yRx\leftrightarrow ⟨x,y⟩\in R^{-1}$$
10		df-br	$$⊢xRy\leftrightarrow ⟨x,y⟩\in R$$
11	4 9 10	3bitr3g	$$⊢R\mathrm{Er}A\to \left(⟨x,y⟩\in R^{-1}\leftrightarrow ⟨x,y⟩\in R\right)$$
12	11	eqrelrdv2	$$⊢\left(\left(\mathrm{Rel}{R}^{-1}\wedge \mathrm{Rel}R\right)\wedge R\mathrm{Er}A\right)\to R^{-1}=R$$
13	2 12	mpanl1	$$⊢\left(\mathrm{Rel}R\wedge R\mathrm{Er}A\right)\to R^{-1}=R$$
14	1 13	mpancom	$$⊢R\mathrm{Er}A\to R^{-1}=R$$