Theorem ereq1

Description: Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995) (Revised by Mario Carneiro, 12-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		releq	$$⊢R=S\to \left(\mathrm{Rel}R\leftrightarrow \mathrm{Rel}S\right)$$
2		dmeq	$$⊢R=S\to \mathrm{dom}R=\mathrm{dom}S$$
3	2	eqeq1d	$$⊢R=S\to \left(\mathrm{dom}R=A\leftrightarrow \mathrm{dom}S=A\right)$$
4		cnveq	$$⊢R=S\to R^{-1}=S^{-1}$$
5		coeq1	$$⊢R=S\to R\circ R=S\circ R$$
6		coeq2	$$⊢R=S\to S\circ R=S\circ S$$
7	5 6	eqtrd	$$⊢R=S\to R\circ R=S\circ S$$
8	4 7	uneq12d	$$⊢R=S\to R^{-1}\cup \left(R\circ R\right)=S^{-1}\cup \left(S\circ S\right)$$
9	8	sseq1d	$$⊢R=S\to \left(R^{-1}\cup \left(R\circ R\right)\subseteq R\leftrightarrow S^{-1}\cup \left(S\circ S\right)\subseteq R\right)$$
10		sseq2	$$⊢R=S\to \left(S^{-1}\cup \left(S\circ S\right)\subseteq R\leftrightarrow S^{-1}\cup \left(S\circ S\right)\subseteq S\right)$$
11	9 10	bitrd	$$⊢R=S\to \left(R^{-1}\cup \left(R\circ R\right)\subseteq R\leftrightarrow S^{-1}\cup \left(S\circ S\right)\subseteq S\right)$$
12	1 3 11	3anbi123d	$$⊢R=S\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}S\wedge \mathrm{dom}S=A\wedge S^{-1}\cup \left(S\circ S\right)\subseteq S\right)\right)$$
13		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)$$
14		df-er	$$⊢S\mathrm{Er}A\leftrightarrow \left(\mathrm{Rel}S\wedge \mathrm{dom}S=A\wedge S^{-1}\cup \left(S\circ S\right)\subseteq S\right)$$
15	12 13 14	3bitr4g	$$⊢R=S\to \left(R\mathrm{Er}A\leftrightarrow S\mathrm{Er}A\right)$$