Theorem ereq2

Description: Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Assertion	ereq2	|- ( A = B -> ( R Er A <-> R Er B ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq2	|- ( A = B -> ( dom R = A <-> dom R = B ) )
2	1	3anbi2d	|- ( A = B -> ( ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) <-> ( Rel R /\ dom R = B /\ ( `' R u. ( R o. R ) ) C_ R ) ) )
3		df-er	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
4		df-er	|- ( R Er B <-> ( Rel R /\ dom R = B /\ ( `' R u. ( R o. R ) ) C_ R ) )
5	2 3 4	3bitr4g	|- ( A = B -> ( R Er A <-> R Er B ) )