Theorem cleq1

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

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

Proof

Step	Hyp	Ref	Expression
1		cleq1lem	$$⊢R=S\to \left(\left(R\subseteq r\wedge \phi \right)\leftrightarrow \left(S\subseteq r\wedge \phi \right)\right)$$
2	1	abbidv	$$⊢R=S\to \left\{r|\left(R\subseteq r\wedge \phi \right)\right\}=\left\{r|\left(S\subseteq r\wedge \phi \right)\right\}$$
3	2	inteqd	$$⊢R=S\to \bigcap \left\{r|\left(R\subseteq r\wedge \phi \right)\right\}=\bigcap \left\{r|\left(S\subseteq r\wedge \phi \right)\right\}$$