This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ersym

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

Ref Expression
Hypotheses ersym.1 ⊢ φ → R Er X
ersym.2 ⊢ φ → A R B
Assertion ersym ⊢ φ → B R A

Proof

Step Hyp Ref Expression
1 ersym.1 ⊢ φ → R Er X
2 ersym.2 ⊢ φ → A R B
3 errel ⊢ R Er X → Rel ⁡ R
4 1 3 syl ⊢ φ → Rel ⁡ R
5 brrelex12 ⊢ Rel ⁡ R ∧ A R B → A ∈ V ∧ B ∈ V
6 4 2 5 syl2anc ⊢ φ → A ∈ V ∧ B ∈ V
7 brcnvg ⊢ B ∈ V ∧ A ∈ V → B R -1 A ↔ A R B
8 7 ancoms ⊢ A ∈ V ∧ B ∈ V → B R -1 A ↔ A R B
9 6 8 syl ⊢ φ → B R -1 A ↔ A R B
10 2 9 mpbird ⊢ φ → B R -1 A
11 df-er ⊢ R Er X ↔ Rel ⁡ R ∧ dom ⁡ R = X ∧ R -1 ∪ R ∘ R ⊆ R
12 11 simp3bi ⊢ R Er X → R -1 ∪ R ∘ R ⊆ R
13 1 12 syl ⊢ φ → R -1 ∪ R ∘ R ⊆ R
14 13 unssad ⊢ φ → R -1 ⊆ R
15 14 ssbrd ⊢ φ → B R -1 A → B R A
16 10 15 mpd ⊢ φ → B R A