# Metamath Proof Explorer

## Theorem erth

Description: Basic property of equivalence relations. Theorem 73 of Suppes p. 82. (Contributed by NM, 23-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses erth.1
`|- ( ph -> R Er X )`
erth.2
`|- ( ph -> A e. X )`
Assertion erth
`|- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )`

### Proof

Step Hyp Ref Expression
1 erth.1
` |-  ( ph -> R Er X )`
2 erth.2
` |-  ( ph -> A e. X )`
3 1 ersymb
` |-  ( ph -> ( A R B <-> B R A ) )`
4 3 biimpa
` |-  ( ( ph /\ A R B ) -> B R A )`
5 1 ertr
` |-  ( ph -> ( ( B R A /\ A R x ) -> B R x ) )`
6 5 impl
` |-  ( ( ( ph /\ B R A ) /\ A R x ) -> B R x )`
7 4 6 syldanl
` |-  ( ( ( ph /\ A R B ) /\ A R x ) -> B R x )`
8 1 ertr
` |-  ( ph -> ( ( A R B /\ B R x ) -> A R x ) )`
9 8 impl
` |-  ( ( ( ph /\ A R B ) /\ B R x ) -> A R x )`
10 7 9 impbida
` |-  ( ( ph /\ A R B ) -> ( A R x <-> B R x ) )`
11 vex
` |-  x e. _V`
` |-  ( ( ph /\ A R B ) -> A e. X )`
13 elecg
` |-  ( ( x e. _V /\ A e. X ) -> ( x e. [ A ] R <-> A R x ) )`
14 11 12 13 sylancr
` |-  ( ( ph /\ A R B ) -> ( x e. [ A ] R <-> A R x ) )`
15 errel
` |-  ( R Er X -> Rel R )`
16 1 15 syl
` |-  ( ph -> Rel R )`
17 brrelex2
` |-  ( ( Rel R /\ A R B ) -> B e. _V )`
18 16 17 sylan
` |-  ( ( ph /\ A R B ) -> B e. _V )`
19 elecg
` |-  ( ( x e. _V /\ B e. _V ) -> ( x e. [ B ] R <-> B R x ) )`
20 11 18 19 sylancr
` |-  ( ( ph /\ A R B ) -> ( x e. [ B ] R <-> B R x ) )`
21 10 14 20 3bitr4d
` |-  ( ( ph /\ A R B ) -> ( x e. [ A ] R <-> x e. [ B ] R ) )`
22 21 eqrdv
` |-  ( ( ph /\ A R B ) -> [ A ] R = [ B ] R )`
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> R Er X )`
24 1 2 erref
` |-  ( ph -> A R A )`
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A R A )`
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A e. X )`
27 elecg
` |-  ( ( A e. X /\ A e. X ) -> ( A e. [ A ] R <-> A R A ) )`
28 26 26 27 syl2anc
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> ( A e. [ A ] R <-> A R A ) )`
29 25 28 mpbird
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A e. [ A ] R )`
30 simpr
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> [ A ] R = [ B ] R )`
31 29 30 eleqtrd
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A e. [ B ] R )`
32 23 30 ereldm
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> ( A e. X <-> B e. X ) )`
33 26 32 mpbid
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> B e. X )`
34 elecg
` |-  ( ( A e. X /\ B e. X ) -> ( A e. [ B ] R <-> B R A ) )`
35 26 33 34 syl2anc
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> ( A e. [ B ] R <-> B R A ) )`
36 31 35 mpbid
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> B R A )`
37 23 36 ersym
` |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A R B )`
38 22 37 impbida
` |-  ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )`