# Metamath Proof Explorer

## 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 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
ersym.2 ${⊢}{\phi }\to {A}{R}{B}$
Assertion ersym ${⊢}{\phi }\to {B}{R}{A}$

### Proof

Step Hyp Ref Expression
1 ersym.1 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
2 ersym.2 ${⊢}{\phi }\to {A}{R}{B}$
3 errel ${⊢}{R}\mathrm{Er}{X}\to \mathrm{Rel}{R}$
4 1 3 syl ${⊢}{\phi }\to \mathrm{Rel}{R}$
5 brrelex12 ${⊢}\left(\mathrm{Rel}{R}\wedge {A}{R}{B}\right)\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
6 4 2 5 syl2anc ${⊢}{\phi }\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
7 brcnvg ${⊢}\left({B}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left({B}{{R}}^{-1}{A}↔{A}{R}{B}\right)$
8 7 ancoms ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left({B}{{R}}^{-1}{A}↔{A}{R}{B}\right)$
9 6 8 syl ${⊢}{\phi }\to \left({B}{{R}}^{-1}{A}↔{A}{R}{B}\right)$
10 2 9 mpbird ${⊢}{\phi }\to {B}{{R}}^{-1}{A}$
11 df-er ${⊢}{R}\mathrm{Er}{X}↔\left(\mathrm{Rel}{R}\wedge \mathrm{dom}{R}={X}\wedge {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}\right)$
12 11 simp3bi ${⊢}{R}\mathrm{Er}{X}\to {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}$
13 1 12 syl ${⊢}{\phi }\to {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}$
14 13 unssad ${⊢}{\phi }\to {{R}}^{-1}\subseteq {R}$
15 14 ssbrd ${⊢}{\phi }\to \left({B}{{R}}^{-1}{A}\to {B}{R}{A}\right)$
16 10 15 mpd ${⊢}{\phi }\to {B}{R}{A}$