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 | |- ( ph -> EqvRel R ) |
|
| Assertion | eqvrelsymb | |- ( ph -> ( A R B <-> B R A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqvrelsymb.1 | |- ( ph -> EqvRel R ) |
|
| 2 | 1 | adantr | |- ( ( ph /\ A R B ) -> EqvRel R ) |
| 3 | simpr | |- ( ( ph /\ A R B ) -> A R B ) |
|
| 4 | 2 3 | eqvrelsym | |- ( ( ph /\ A R B ) -> B R A ) |
| 5 | 1 | adantr | |- ( ( ph /\ B R A ) -> EqvRel R ) |
| 6 | simpr | |- ( ( ph /\ B R A ) -> B R A ) |
|
| 7 | 5 6 | eqvrelsym | |- ( ( ph /\ B R A ) -> A R B ) |
| 8 | 4 7 | impbida | |- ( ph -> ( A R B <-> B R A ) ) |