Metamath Proof Explorer


Theorem erth2

Description: Basic property of equivalence relations. Compare Theorem 73 of Suppes p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015)

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

Proof

Step Hyp Ref Expression
1 erth2.1
 |-  ( ph -> R Er X )
2 erth2.2
 |-  ( ph -> B e. X )
3 1 ersymb
 |-  ( ph -> ( A R B <-> B R A ) )
4 1 2 erth
 |-  ( ph -> ( B R A <-> [ B ] R = [ A ] R ) )
5 eqcom
 |-  ( [ B ] R = [ A ] R <-> [ A ] R = [ B ] R )
6 4 5 bitrdi
 |-  ( ph -> ( B R A <-> [ A ] R = [ B ] R ) )
7 3 6 bitrd
 |-  ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )