Theorem 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	⊢ ( 𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		refreleq	⊢ ( 𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆 ) )
2		symreleq	⊢ ( 𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆 ) )
3		trreleq	⊢ ( 𝑅 = 𝑆 → ( TrRel 𝑅 ↔ TrRel 𝑆 ) )
4	1 2 3	3anbi123d	⊢ ( 𝑅 = 𝑆 → ( ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) ↔ ( RefRel 𝑆 ∧ SymRel 𝑆 ∧ TrRel 𝑆 ) ) )
5		df-eqvrel	⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )
6		df-eqvrel	⊢ ( EqvRel 𝑆 ↔ ( RefRel 𝑆 ∧ SymRel 𝑆 ∧ TrRel 𝑆 ) )
7	4 5 6	3bitr4g	⊢ ( 𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆 ) )