Metamath Proof Explorer


Theorem eqvrelsym

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

Ref Expression
Hypotheses eqvrelsym.1 ( 𝜑 → EqvRel 𝑅 )
eqvrelsym.2 ( 𝜑𝐴 𝑅 𝐵 )
Assertion eqvrelsym ( 𝜑𝐵 𝑅 𝐴 )

Proof

Step Hyp Ref Expression
1 eqvrelsym.1 ( 𝜑 → EqvRel 𝑅 )
2 eqvrelsym.2 ( 𝜑𝐴 𝑅 𝐵 )
3 eqvrelrel ( EqvRel 𝑅 → Rel 𝑅 )
4 relbrcnvg ( Rel 𝑅 → ( 𝐵 𝑅 𝐴𝐴 𝑅 𝐵 ) )
5 1 3 4 3syl ( 𝜑 → ( 𝐵 𝑅 𝐴𝐴 𝑅 𝐵 ) )
6 2 5 mpbird ( 𝜑𝐵 𝑅 𝐴 )
7 eqvrelsymrel ( EqvRel 𝑅 → SymRel 𝑅 )
8 dfsymrel2 ( SymRel 𝑅 ↔ ( 𝑅𝑅 ∧ Rel 𝑅 ) )
9 8 simplbi ( SymRel 𝑅 𝑅𝑅 )
10 1 7 9 3syl ( 𝜑 𝑅𝑅 )
11 10 ssbrd ( 𝜑 → ( 𝐵 𝑅 𝐴𝐵 𝑅 𝐴 ) )
12 6 11 mpd ( 𝜑𝐵 𝑅 𝐴 )