This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 Er 𝐴 → ◡ 𝑅 = 𝑅 )

Proof

Step Hyp Ref Expression
1 errel ⊢ ( 𝑅 Er 𝐴 → Rel 𝑅 )
2 relcnv ⊢ Rel ◡ 𝑅
3 id ⊢ ( 𝑅 Er 𝐴 → 𝑅 Er 𝐴 )
4 3 ersymb ⊢ ( 𝑅 Er 𝐴 → ( 𝑦 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
5 vex ⊢ 𝑥 ∈ V
6 vex ⊢ 𝑦 ∈ V
7 5 6 brcnv ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
8 df-br ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 )
9 7 8 bitr3i ⊢ ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 )
10 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
11 4 9 10 3bitr3g ⊢ ( 𝑅 Er 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
12 11 eqrelrdv2 ⊢ ( ( ( Rel ◡ 𝑅 ∧ Rel 𝑅 ) ∧ 𝑅 Er 𝐴 ) → ◡ 𝑅 = 𝑅 )
13 2 12 mpanl1 ⊢ ( ( Rel 𝑅 ∧ 𝑅 Er 𝐴 ) → ◡ 𝑅 = 𝑅 )
14 1 13 mpancom ⊢ ( 𝑅 Er 𝐴 → ◡ 𝑅 = 𝑅 )