Theorem trcleq1

Description: Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020)

	Ref	Expression
Assertion	trcleq1	$$⊢R=S\to \bigcap \left\{r|\left(R\subseteq r\wedge r\circ r\subseteq r\right)\right\}=\bigcap \left\{r|\left(S\subseteq r\wedge r\circ r\subseteq r\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cleq1	$$⊢R=S\to \bigcap \left\{r|\left(R\subseteq r\wedge r\circ r\subseteq r\right)\right\}=\bigcap \left\{r|\left(S\subseteq r\wedge r\circ r\subseteq r\right)\right\}$$