Theorem ereq2

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

	Ref	Expression
Assertion	ereq2	$$⊢A=B\to \left(R\mathrm{Er}A\leftrightarrow R\mathrm{Er}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$$⊢A=B\to \left(\mathrm{dom}R=A\leftrightarrow \mathrm{dom}R=B\right)$$
2	1	3anbi2d	$$⊢A=B\to \left(\left(\mathrm{Rel}R\wedge \mathrm{dom}R=A\wedge R^{-1}\cup \left(R\circ R\right)\subseteq R\right)\leftrightarrow \left(\mathrm{Rel}R\wedge \mathrm{dom}R=B\wedge R^{-1}\cup \left(R\circ R\right)\subseteq R\right)\right)$$
3		df-er	$$⊢R\mathrm{Er}A\leftrightarrow \left(\mathrm{Rel}R\wedge \mathrm{dom}R=A\wedge R^{-1}\cup \left(R\circ R\right)\subseteq R\right)$$
4		df-er	$$⊢R\mathrm{Er}B\leftrightarrow \left(\mathrm{Rel}R\wedge \mathrm{dom}R=B\wedge R^{-1}\cup \left(R\circ R\right)\subseteq R\right)$$
5	2 3 4	3bitr4g	$$⊢A=B\to \left(R\mathrm{Er}A\leftrightarrow R\mathrm{Er}B\right)$$