Theorem eqvrelsym

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

	Ref	Expression
Hypotheses	eqvrelsym.1	$$⊢\phi \to EqvRelR$$
	eqvrelsym.2	$$⊢\phi \to ARB$$
Assertion	eqvrelsym	$$⊢\phi \to BRA$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelsym.1	$$⊢\phi \to EqvRelR$$
2		eqvrelsym.2	$$⊢\phi \to ARB$$
3		eqvrelrel	$$⊢EqvRelR\to \mathrm{Rel}R$$
4		relbrcnvg	$$⊢\mathrm{Rel}R\to \left(B{R}^{-1}A\leftrightarrow ARB\right)$$
5	1 3 4	3syl	$$⊢\phi \to \left(B{R}^{-1}A\leftrightarrow ARB\right)$$
6	2 5	mpbird	$$⊢\phi \to B{R}^{-1}A$$
7		eqvrelsymrel	$$⊢EqvRelR\to SymRelR$$
8		dfsymrel2	$$⊢SymRelR\leftrightarrow \left(R^{-1}\subseteq R\wedge \mathrm{Rel}R\right)$$
9	8	simplbi	$$⊢SymRelR\to R^{-1}\subseteq R$$
10	1 7 9	3syl	$$⊢\phi \to R^{-1}\subseteq R$$
11	10	ssbrd	$$⊢\phi \to \left(B{R}^{-1}A\to BRA\right)$$
12	6 11	mpd	$$⊢\phi \to BRA$$