ereq2

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

		Ref	Expression
	Assertion	ereq2	$⊢ A = B \to (R Er A \leftrightarrow R Er B)$

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

Metamath Proof Explorer