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

Metamath Proof Explorer

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 )