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 )