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 (R Er A \leftrightarrow S Er A)$

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

Metamath Proof Explorer