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 ( 𝜑𝑅 Er 𝑋 )
erth2.2 ( 𝜑𝐵𝑋 )
Assertion erth2 ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )

Proof

Step Hyp Ref Expression
1 erth2.1 ( 𝜑𝑅 Er 𝑋 )
2 erth2.2 ( 𝜑𝐵𝑋 )
3 1 ersymb ( 𝜑 → ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐴 ) )
4 1 2 erth ( 𝜑 → ( 𝐵 𝑅 𝐴 ↔ [ 𝐵 ] 𝑅 = [ 𝐴 ] 𝑅 ) )
5 eqcom ( [ 𝐵 ] 𝑅 = [ 𝐴 ] 𝑅 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
6 4 5 bitrdi ( 𝜑 → ( 𝐵 𝑅 𝐴 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
7 3 6 bitrd ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )