Theorem erth2

Description: Basic property of equivalence relations. Compare Theorem 73 of Suppes p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015)

	Ref	Expression
Hypotheses	erth2.1	|- ( ph -> R Er X )
	erth2.2	|- ( ph -> B e. X )
Assertion	erth2	|- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )

Proof

Step	Hyp	Ref	Expression
1		erth2.1	|- ( ph -> R Er X )
2		erth2.2	|- ( ph -> B e. X )
3	1	ersymb	|- ( ph -> ( A R B <-> B R A ) )
4	1 2	erth	|- ( ph -> ( B R A <-> [ B ] R = [ A ] R ) )
5		eqcom	|- ( [ B ] R = [ A ] R <-> [ A ] R = [ B ] R )
6	4 5	bitrdi	|- ( ph -> ( B R A <-> [ A ] R = [ B ] R ) )
7	3 6	bitrd	|- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )