Theorem cvbtrcl

Description: Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020)

	Ref	Expression
Assertion	cvbtrcl	$$⊢\left\{x|\left(R\subseteq x\wedge x\circ x\subseteq x\right)\right\}=\left\{y|\left(R\subseteq y\wedge y\circ y\subseteq y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		trcleq2lem	$$⊢x=y\to \left(\left(R\subseteq x\wedge x\circ x\subseteq x\right)\leftrightarrow \left(R\subseteq y\wedge y\circ y\subseteq y\right)\right)$$
2	1	cbvabv	$$⊢\left\{x|\left(R\subseteq x\wedge x\circ x\subseteq x\right)\right\}=\left\{y|\left(R\subseteq y\wedge y\circ y\subseteq y\right)\right\}$$