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
12 2 adantr 
 |-  ( ( 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 )
23 1 adantr 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> R Er X )
24 1 2 erref 
 |-  ( ph -> A R A )
25 24 adantr 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A R A )
26 2 adantr 
 |-  ( ( 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 ) )