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 ARB$$
Assertion	ersym	$$⊢\phi \to BRA$$

Proof

Step	Hyp	Ref	Expression
1		ersym.1	$$⊢\phi \to R\mathrm{Er}X$$
2		ersym.2	$$⊢\phi \to ARB$$
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 ARB\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\leftrightarrow ARB\right)$$
8	7	ancoms	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(B{R}^{-1}A\leftrightarrow ARB\right)$$
9	6 8	syl	$$⊢\phi \to \left(B{R}^{-1}A\leftrightarrow ARB\right)$$
10	2 9	mpbird	$$⊢\phi \to B{R}^{-1}A$$
11		df-er	$$⊢R\mathrm{Er}X\leftrightarrow \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 BRA\right)$$
16	10 15	mpd	$$⊢\phi \to BRA$$