Theorem cbvcllem

Description: Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020)

	Ref	Expression
Hypothesis	cbvcllem.y	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvcllem	$$⊢\left\{x|\left(X\subseteq x\wedge \phi \right)\right\}=\left\{y|\left(X\subseteq y\wedge \psi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvcllem.y	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2	1	cleq2lem	$$⊢x=y\to \left(\left(X\subseteq x\wedge \phi \right)\leftrightarrow \left(X\subseteq y\wedge \psi \right)\right)$$
3	2	cbvabv	$$⊢\left\{x|\left(X\subseteq x\wedge \phi \right)\right\}=\left\{y|\left(X\subseteq y\wedge \psi \right)\right\}$$