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
|- ( ph -> R Er X )
Assertion ersymb
|- ( ph -> ( A R B <-> B R A ) )

Proof

Step Hyp Ref Expression
1 ersymb.1
 |-  ( ph -> R Er X )
2 1 adantr
 |-  ( ( ph /\ A R B ) -> R Er X )
3 simpr
 |-  ( ( ph /\ A R B ) -> A R B )
4 2 3 ersym
 |-  ( ( ph /\ A R B ) -> B R A )
5 1 adantr
 |-  ( ( ph /\ B R A ) -> R Er X )
6 simpr
 |-  ( ( ph /\ B R A ) -> B R A )
7 5 6 ersym
 |-  ( ( ph /\ B R A ) -> A R B )
8 4 7 impbida
 |-  ( ph -> ( A R B <-> B R A ) )