Theorem symreleq

Description: Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019) (Revised by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	symreleq	$$⊢R=S\to \left(SymRelR\leftrightarrow SymRelS\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnveq	$$⊢R=S\to R^{-1}=S^{-1}$$
2		id	$$⊢R=S\to R=S$$
3	1 2	sseq12d	$$⊢R=S\to \left(R^{-1}\subseteq R\leftrightarrow S^{-1}\subseteq S\right)$$
4		releq	$$⊢R=S\to \left(\mathrm{Rel}R\leftrightarrow \mathrm{Rel}S\right)$$
5	3 4	anbi12d	$$⊢R=S\to \left(\left(R^{-1}\subseteq R\wedge \mathrm{Rel}R\right)\leftrightarrow \left(S^{-1}\subseteq S\wedge \mathrm{Rel}S\right)\right)$$
6		dfsymrel2	$$⊢SymRelR\leftrightarrow \left(R^{-1}\subseteq R\wedge \mathrm{Rel}R\right)$$
7		dfsymrel2	$$⊢SymRelS\leftrightarrow \left(S^{-1}\subseteq S\wedge \mathrm{Rel}S\right)$$
8	5 6 7	3bitr4g	$$⊢R=S\to \left(SymRelR\leftrightarrow SymRelS\right)$$