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 | ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) ) |
| 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 | ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) ) |