# Metamath Proof Explorer

## 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({y}{R}{x}↔{x}{R}{y}\right)$
5 vex ${⊢}{x}\in \mathrm{V}$
6 vex ${⊢}{y}\in \mathrm{V}$
7 5 6 brcnv ${⊢}{x}{{R}}^{-1}{y}↔{y}{R}{x}$
8 df-br ${⊢}{x}{{R}}^{-1}{y}↔⟨{x},{y}⟩\in {{R}}^{-1}$
9 7 8 bitr3i ${⊢}{y}{R}{x}↔⟨{x},{y}⟩\in {{R}}^{-1}$
10 df-br ${⊢}{x}{R}{y}↔⟨{x},{y}⟩\in {R}$
11 4 9 10 3bitr3g ${⊢}{R}\mathrm{Er}{A}\to \left(⟨{x},{y}⟩\in {{R}}^{-1}↔⟨{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}$