This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to EqvRel R$
		eqvrelsym.2	$⊢ φ \to A R B$
	Assertion	eqvrelsym	$⊢ φ \to B R A$

Proof

Step	Hyp	Ref	Expression
1		eqvrelsym.1	$⊢ φ \to EqvRel R$
2		eqvrelsym.2	$⊢ φ \to A R B$
3		eqvrelrel	$⊢ EqvRel R \to Rel R$
4		relbrcnvg	$⊢ Rel R \to (B R^{-1} A \leftrightarrow A R B)$
5	1 3 4	3syl	$⊢ φ \to (B R^{-1} A \leftrightarrow A R B)$
6	2 5	mpbird	$⊢ φ \to B R^{-1} A$
7		eqvrelsymrel	$⊢ EqvRel R \to SymRel R$
8		dfsymrel2	$⊢ SymRel R \leftrightarrow (R^{-1} \subseteq R \land Rel R)$
9	8	simplbi	$⊢ SymRel R \to R^{-1} \subseteq R$
10	1 7 9	3syl	$⊢ φ \to R^{-1} \subseteq R$
11	10	ssbrd	$⊢ φ \to (B R^{-1} A \to B R A)$
12	6 11	mpd	$⊢ φ \to B R A$