Theorem cbvabv

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999) Require x , y be disjoint to avoid ax-11 and ax-13 . (Revised by Steven Nguyen, 4-Dec-2022)

	Ref	Expression
Hypothesis	cbvabv.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvabv	$$⊢\left\{x|\phi \right\}=\left\{y|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvabv.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2	1	cbvsbv	$$⊢\left[z/x\right]\phi \leftrightarrow \left[z/y\right]\psi$$
3		df-clab	$$⊢z\in \left\{x|\phi \right\}\leftrightarrow \left[z/x\right]\phi$$
4		df-clab	$$⊢z\in \left\{y|\psi \right\}\leftrightarrow \left[z/y\right]\psi$$
5	2 3 4	3bitr4i	$$⊢z\in \left\{x|\phi \right\}\leftrightarrow z\in \left\{y|\psi \right\}$$
6	5	eqriv	$$⊢\left\{x|\phi \right\}=\left\{y|\psi \right\}$$