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