Theorem ersym

Description: An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	ersym.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
	ersym.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion	ersym	⊢ ( 𝜑 → 𝐵 𝑅 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ersym.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2		ersym.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3		errel	⊢ ( 𝑅 Er 𝑋 → Rel 𝑅 )
4	1 3	syl	⊢ ( 𝜑 → Rel 𝑅 )
5		brrelex12	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
6	4 2 5	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
7		brcnvg	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐵 ◡ 𝑅 𝐴 ↔ 𝐴 𝑅 𝐵 ) )
8	7	ancoms	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐵 ◡ 𝑅 𝐴 ↔ 𝐴 𝑅 𝐵 ) )
9	6 8	syl	⊢ ( 𝜑 → ( 𝐵 ◡ 𝑅 𝐴 ↔ 𝐴 𝑅 𝐵 ) )
10	2 9	mpbird	⊢ ( 𝜑 → 𝐵 ◡ 𝑅 𝐴 )
11		df-er	⊢ ( 𝑅 Er 𝑋 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )
12	11	simp3bi	⊢ ( 𝑅 Er 𝑋 → ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
13	1 12	syl	⊢ ( 𝜑 → ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
14	13	unssad	⊢ ( 𝜑 → ◡ 𝑅 ⊆ 𝑅 )
15	14	ssbrd	⊢ ( 𝜑 → ( 𝐵 ◡ 𝑅 𝐴 → 𝐵 𝑅 𝐴 ) )
16	10 15	mpd	⊢ ( 𝜑 → 𝐵 𝑅 𝐴 )