This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cleq1

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

		Ref	Expression
	Assertion	cleq1	$⊢ R = S \to ⋂ \{r \| (R \subseteq r \land φ)\} = ⋂ \{r \| (S \subseteq r \land φ)\}$

Step	Hyp	Ref	Expression
1		cleq1lem	$⊢ R = S \to ((R \subseteq r \land φ) \leftrightarrow (S \subseteq r \land φ))$
2	1	abbidv	$⊢ R = S \to \{r \| (R \subseteq r \land φ)\} = \{r \| (S \subseteq r \land φ)\}$
3	2	inteqd	$⊢ R = S \to ⋂ \{r \| (R \subseteq r \land φ)\} = ⋂ \{r \| (S \subseteq r \land φ)\}$