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		sbco2vv	$$⊢\left[z/y\right]\left[y/x\right]\phi \leftrightarrow \left[z/x\right]\phi$$
3	1	sbievw	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
4	3	sbbii	$$⊢\left[z/y\right]\left[y/x\right]\phi \leftrightarrow \left[z/y\right]\psi$$
5	2 4	bitr3i	$$⊢\left[z/x\right]\phi \leftrightarrow \left[z/y\right]\psi$$
6		df-clab	$$⊢z\in \left\{x|\phi \right\}\leftrightarrow \left[z/x\right]\phi$$
7		df-clab	$$⊢z\in \left\{y|\psi \right\}\leftrightarrow \left[z/y\right]\psi$$
8	5 6 7	3bitr4i	$$⊢z\in \left\{x|\phi \right\}\leftrightarrow z\in \left\{y|\psi \right\}$$
9	8	eqriv	$$⊢\left\{x|\phi \right\}=\left\{y|\psi \right\}$$