eqvreleq

Description: Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 23-Sep-2021)

		Ref	Expression
	Assertion	eqvreleq	$⊢ R = S \to (EqvRel R \leftrightarrow EqvRel S)$

Step	Hyp	Ref	Expression
1		refreleq	$⊢ R = S \to (RefRel R \leftrightarrow RefRel S)$
2		symreleq	$⊢ R = S \to (SymRel R \leftrightarrow SymRel S)$
3		trreleq	$⊢ R = S \to (TrRel R \leftrightarrow TrRel S)$
4	1 2 3	3anbi123d	$⊢ R = S \to ((RefRel R \land SymRel R \land TrRel R) \leftrightarrow (RefRel S \land SymRel S \land TrRel S))$
5		df-eqvrel	$⊢ EqvRel R \leftrightarrow (RefRel R \land SymRel R \land TrRel R)$
6		df-eqvrel	$⊢ EqvRel S \leftrightarrow (RefRel S \land SymRel S \land TrRel S)$
7	4 5 6	3bitr4g	$⊢ R = S \to (EqvRel R \leftrightarrow EqvRel S)$

Metamath Proof Explorer