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 Er A -> `' R = R )

Proof

Step Hyp Ref Expression
1 errel 
 |-  ( R Er A -> Rel R )
2 relcnv 
 |-  Rel `' R
3 id 
 |-  ( R Er A -> R Er A )
4 3 ersymb 
 |-  ( R Er A -> ( y R x <-> x R y ) )
5 vex 
 |-  x e. _V
6 vex 
 |-  y e. _V
7 5 6 brcnv 
 |-  ( x `' R y <-> y R x )
8 df-br 
 |-  ( x `' R y <-> <. x , y >. e. `' R )
9 7 8 bitr3i 
 |-  ( y R x <-> <. x , y >. e. `' R )
10 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
11 4 9 10 3bitr3g 
 |-  ( R Er A -> ( <. x , y >. e. `' R <-> <. x , y >. e. R ) )
12 11 eqrelrdv2 
 |-  ( ( ( Rel `' R /\ Rel R ) /\ R Er A ) -> `' R = R )
13 2 12 mpanl1 
 |-  ( ( Rel R /\ R Er A ) -> `' R = R )
14 1 13 mpancom 
 |-  ( R Er A -> `' R = R )