Metamath Proof Explorer

Theorem ersymb

Description: An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis ersymb.1 ⊢ φ → R Er X
Assertion ersymb ⊢ φ → A R B ↔ B R A

Proof

Step Hyp Ref Expression
1 ersymb.1 ⊢ φ → R Er X
2 1 adantr ⊢ φ ∧ A R B → R Er X
3 simpr ⊢ φ ∧ A R B → A R B
4 2 3 ersym ⊢ φ ∧ A R B → B R A
5 1 adantr ⊢ φ ∧ B R A → R Er X
6 simpr ⊢ φ ∧ B R A → B R A
7 5 6 ersym ⊢ φ ∧ B R A → A R B
8 4 7 impbida ⊢ φ → A R B ↔ B R A