Theorem eqvrelthi

Description: Basic property of equivalence relations. Part of Lemma 3N of Enderton p. 57. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvrelthi.1	|- ( ph -> EqvRel R )
	eqvrelthi.2	|- ( ph -> A R B )
Assertion	eqvrelthi	|- ( ph -> [ A ] R = [ B ] R )

Proof

Step	Hyp	Ref	Expression
1		eqvrelthi.1	|- ( ph -> EqvRel R )
2		eqvrelthi.2	|- ( ph -> A R B )
3	1 2	eqvrelcl	|- ( ph -> A e. dom R )
4	1 3	eqvrelth	|- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )
5	2 4	mpbid	|- ( ph -> [ A ] R = [ B ] R )