# 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 )`
` |-  ( ph -> `' R C_ R )`
` |-  ( ph -> ( B `' R A -> B R A ) )`
` |-  ( ph -> B R A )`