Theorem cbviota

Description: Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbviotaw when possible. (Contributed by Andrew Salmon, 1-Aug-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbviota.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	cbviota.2	$$⊢Ⅎy\phi$$
	cbviota.3	$$⊢Ⅎx\psi$$
Assertion	cbviota	$$⊢\left(\iota x|\phi \right)=\left(\iota y|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		cbviota.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		cbviota.2	$$⊢Ⅎy\phi$$
3		cbviota.3	$$⊢Ⅎx\psi$$
4		nfv	$$⊢Ⅎz\left(\phi \leftrightarrow x=w\right)$$
5		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
6		nfv	$$⊢Ⅎxz=w$$
7	5 6	nfbi	$$⊢Ⅎx\left(\left[z/x\right]\phi \leftrightarrow z=w\right)$$
8		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
9		equequ1	$$⊢x=z\to \left(x=w\leftrightarrow z=w\right)$$
10	8 9	bibi12d	$$⊢x=z\to \left(\left(\phi \leftrightarrow x=w\right)\leftrightarrow \left(\left[z/x\right]\phi \leftrightarrow z=w\right)\right)$$
11	4 7 10	cbvalv1	$$⊢\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \forall z\left(\left[z/x\right]\phi \leftrightarrow z=w\right)$$
12	2	nfsb	$$⊢Ⅎy\left[z/x\right]\phi$$
13		nfv	$$⊢Ⅎyz=w$$
14	12 13	nfbi	$$⊢Ⅎy\left(\left[z/x\right]\phi \leftrightarrow z=w\right)$$
15		nfv	$$⊢Ⅎz\left(\psi \leftrightarrow y=w\right)$$
16		sbequ	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
17	3 1	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
18	16 17	bitrdi	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
19		equequ1	$$⊢z=y\to \left(z=w\leftrightarrow y=w\right)$$
20	18 19	bibi12d	$$⊢z=y\to \left(\left(\left[z/x\right]\phi \leftrightarrow z=w\right)\leftrightarrow \left(\psi \leftrightarrow y=w\right)\right)$$
21	14 15 20	cbvalv1	$$⊢\forall z\left(\left[z/x\right]\phi \leftrightarrow z=w\right)\leftrightarrow \forall y\left(\psi \leftrightarrow y=w\right)$$
22	11 21	bitri	$$⊢\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \forall y\left(\psi \leftrightarrow y=w\right)$$
23	22	abbii	$$⊢\left\{w|\forall x\left(\phi \leftrightarrow x=w\right)\right\}=\left\{w|\forall y\left(\psi \leftrightarrow y=w\right)\right\}$$
24	23	unieqi	$$⊢\bigcup \left\{w|\forall x\left(\phi \leftrightarrow x=w\right)\right\}=\bigcup \left\{w|\forall y\left(\psi \leftrightarrow y=w\right)\right\}$$
25		dfiota2	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{w|\forall x\left(\phi \leftrightarrow x=w\right)\right\}$$
26		dfiota2	$$⊢\left(\iota y|\psi \right)=\bigcup \left\{w|\forall y\left(\psi \leftrightarrow y=w\right)\right\}$$
27	24 25 26	3eqtr4i	$$⊢\left(\iota x|\phi \right)=\left(\iota y|\psi \right)$$