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 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
ersym.2 ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion ersym ( 𝜑 → 𝐵 𝑅 𝐴 )

Proof

Step Hyp Ref Expression
1 ersym.1 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2 ersym.2 ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3 errel ⊢ ( 𝑅 Er 𝑋 → Rel 𝑅 )
4 1 3 syl ⊢ ( 𝜑 → Rel 𝑅 )
5 brrelex12 ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
6 4 2 5 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
7 brcnvg ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐵 ◡ 𝑅 𝐴 ↔ 𝐴 𝑅 𝐵 ) )
8 7 ancoms ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐵 ◡ 𝑅 𝐴 ↔ 𝐴 𝑅 𝐵 ) )
9 6 8 syl ⊢ ( 𝜑 → ( 𝐵 ◡ 𝑅 𝐴 ↔ 𝐴 𝑅 𝐵 ) )
10 2 9 mpbird ⊢ ( 𝜑 → 𝐵 ◡ 𝑅 𝐴 )
11 df-er ⊢ ( 𝑅 Er 𝑋 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )
12 11 simp3bi ⊢ ( 𝑅 Er 𝑋 → ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
13 1 12 syl ⊢ ( 𝜑 → ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
14 13 unssad ⊢ ( 𝜑 → ◡ 𝑅 ⊆ 𝑅 )
15 14 ssbrd ⊢ ( 𝜑 → ( 𝐵 ◡ 𝑅 𝐴 → 𝐵 𝑅 𝐴 ) )
16 10 15 mpd ⊢ ( 𝜑 → 𝐵 𝑅 𝐴 )