Theorem cbvsbcw

Description: Change bound variables in a wff substitution. Version of cbvsbc with a disjoint variable condition, which does not require ax-13 . (Contributed by Jeff Hankins, 19-Sep-2009) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbvsbcw.1	$$⊢Ⅎy\phi$$
	cbvsbcw.2	$$⊢Ⅎx\psi$$
	cbvsbcw.3	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvsbcw	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvsbcw.1	$$⊢Ⅎy\phi$$
2		cbvsbcw.2	$$⊢Ⅎx\psi$$
3		cbvsbcw.3	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
4	1 2 3	cbvabw	$$⊢\left\{x|\phi \right\}=\left\{y|\psi \right\}$$
5	4	eleq2i	$$⊢A\in \left\{x|\phi \right\}\leftrightarrow A\in \left\{y|\psi \right\}$$
6		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow A\in \left\{x|\phi \right\}$$
7		df-sbc	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\psi \leftrightarrow A\in \left\{y|\psi \right\}$$
8	5 6 7	3bitr4i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\psi$$