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	|- ( ph -> R Er X )
	ersym.2	|- ( ph -> A R B )
Assertion	ersym	|- ( ph -> B R A )

Proof

Step	Hyp	Ref	Expression
1		ersym.1	|- ( ph -> R Er X )
2		ersym.2	|- ( ph -> A R B )
3		errel	|- ( R Er X -> Rel R )
4	1 3	syl	|- ( ph -> Rel R )
5		brrelex12	|- ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )
6	4 2 5	syl2anc	|- ( ph -> ( A e. _V /\ B e. _V ) )
7		brcnvg	|- ( ( B e. _V /\ A e. _V ) -> ( B `' R A <-> A R B ) )
8	7	ancoms	|- ( ( A e. _V /\ B e. _V ) -> ( B `' R A <-> A R B ) )
9	6 8	syl	|- ( ph -> ( B `' R A <-> A R B ) )
10	2 9	mpbird	|- ( ph -> B `' R A )
11		df-er	|- ( R Er X <-> ( Rel R /\ dom R = X /\ ( `' R u. ( R o. R ) ) C_ R ) )
12	11	simp3bi	|- ( R Er X -> ( `' R u. ( R o. R ) ) C_ R )
13	1 12	syl	|- ( ph -> ( `' R u. ( R o. R ) ) C_ R )
14	13	unssad	|- ( ph -> `' R C_ R )
15	14	ssbrd	|- ( ph -> ( B `' R A -> B R A ) )
16	10 15	mpd	|- ( ph -> B R A )