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	|- ( ph -> EqvRel R )
	eqvrelsym.2	|- ( ph -> A R B )
Assertion	eqvrelsym	|- ( ph -> B R A )

Proof

Step	Hyp	Ref	Expression
1		eqvrelsym.1	|- ( ph -> EqvRel R )
2		eqvrelsym.2	|- ( ph -> A R B )
3		eqvrelrel	|- ( EqvRel R -> Rel R )
4		relbrcnvg	|- ( Rel R -> ( B `' R A <-> A R B ) )
5	1 3 4	3syl	|- ( ph -> ( B `' R A <-> A R B ) )
6	2 5	mpbird	|- ( ph -> B `' R A )
7		eqvrelsymrel	|- ( EqvRel R -> SymRel R )
8		dfsymrel2	|- ( SymRel R <-> ( `' R C_ R /\ Rel R ) )
9	8	simplbi	|- ( SymRel R -> `' R C_ R )
10	1 7 9	3syl	|- ( ph -> `' R C_ R )
11	10	ssbrd	|- ( ph -> ( B `' R A -> B R A ) )
12	6 11	mpd	|- ( ph -> B R A )