Description: An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 12-Aug-2015) (Revised and distinct variable conditions removed by Peter Mazsa, 2-Jun-2019.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eqvrelsymb.1 | ⊢ ( 𝜑 → EqvRel 𝑅 ) | |
| Assertion | eqvrelsymb | ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqvrelsymb.1 | ⊢ ( 𝜑 → EqvRel 𝑅 ) | |
| 2 | 1 | adantr | ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → EqvRel 𝑅 ) |
| 3 | simpr | ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 ) | |
| 4 | 2 3 | eqvrelsym | ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 𝑅 𝐴 ) |
| 5 | 1 | adantr | ⊢ ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) → EqvRel 𝑅 ) |
| 6 | simpr | ⊢ ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) → 𝐵 𝑅 𝐴 ) | |
| 7 | 5 6 | eqvrelsym | ⊢ ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 𝑅 𝐵 ) |
| 8 | 4 7 | impbida | ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) ) |