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

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 
|- ( ph -> EqvRel R )
eqvrelsym.2 
|- ( ph -> A R B )
Assertion eqvrelsym 
|- ( ph -> B R A )

Proof

Step Hyp Ref Expression
1 eqvrelsym.1 
 |-  ( ph -> EqvRel R )
2 eqvrelsym.2 
 |-  ( ph -> A R B )
3 eqvrelrel 
 |-  ( EqvRel R -> Rel R )
4 relbrcnvg 
 |-  ( Rel R -> ( B `' R A <-> A R B ) )
5 1 3 4 3syl 
 |-  ( ph -> ( B `' R A <-> A R B ) )
6 2 5 mpbird 
 |-  ( ph -> B `' R A )
7 eqvrelsymrel 
 |-  ( EqvRel R -> SymRel R )
8 dfsymrel2 
 |-  ( SymRel R <-> ( `' R C_ R /\ Rel R ) )
9 8 simplbi 
 |-  ( SymRel R -> `' R C_ R )
10 1 7 9 3syl 
 |-  ( ph -> `' R C_ R )
11 10 ssbrd 
 |-  ( ph -> ( B `' R A -> B R A ) )
12 6 11 mpd 
 |-  ( ph -> B R A )