Metamath Proof Explorer

Theorem eqvrelsymb

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 R
Assertion eqvrelsymb ⊢ φ → A R B ↔ B R A

Proof

Step Hyp Ref Expression
1 eqvrelsymb.1 ⊢ φ → EqvRel R
2 1 adantr ⊢ φ ∧ A R B → EqvRel R
3 simpr ⊢ φ ∧ A R B → A R B
4 2 3 eqvrelsym ⊢ φ ∧ A R B → B R A
5 1 adantr ⊢ φ ∧ B R A → EqvRel R
6 simpr ⊢ φ ∧ B R A → B R A
7 5 6 eqvrelsym ⊢ φ ∧ B R A → A R B
8 4 7 impbida ⊢ φ → A R B ↔ B R A