Theorem cbvsbc

Description: Change bound variables in a wff substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvsbcw when possible. (Contributed by Jeff Hankins, 19-Sep-2009) (Proof shortened by Andrew Salmon, 8-Jun-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvsbc.1	$$⊢Ⅎy\phi$$
2		cbvsbc.2	$$⊢Ⅎx\psi$$
3		cbvsbc.3	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
4	1 2 3	cbvab	$$⊢\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$$