Theorem trreleq

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

	Ref	Expression
Assertion	trreleq	$$⊢R=S\to \left(TrRelR\leftrightarrow TrRelS\right)$$

Proof

Step	Hyp	Ref	Expression
1		coideq	$$⊢R=S\to R\circ R=S\circ S$$
2		id	$$⊢R=S\to R=S$$
3	1 2	sseq12d	$$⊢R=S\to \left(R\circ R\subseteq R\leftrightarrow S\circ S\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\circ R\subseteq R\wedge \mathrm{Rel}R\right)\leftrightarrow \left(S\circ S\subseteq S\wedge \mathrm{Rel}S\right)\right)$$
6		dftrrel2	$$⊢TrRelR\leftrightarrow \left(R\circ R\subseteq R\wedge \mathrm{Rel}R\right)$$
7		dftrrel2	$$⊢TrRelS\leftrightarrow \left(S\circ S\subseteq S\wedge \mathrm{Rel}S\right)$$
8	5 6 7	3bitr4g	$$⊢R=S\to \left(TrRelR\leftrightarrow TrRelS\right)$$