Theorem cbviotaw

Description: Change bound variables in a description binder. Version of cbviota with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 1-Aug-2011) Avoid ax-13 . (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbviotaw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		cbviotaw.2	$$⊢Ⅎy\phi$$
3		cbviotaw.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	nfsbv	$$⊢Ⅎ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	3 1	sbhypf	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
17		equequ1	$$⊢z=y\to \left(z=w\leftrightarrow y=w\right)$$
18	16 17	bibi12d	$$⊢z=y\to \left(\left(\left[z/x\right]\phi \leftrightarrow z=w\right)\leftrightarrow \left(\psi \leftrightarrow y=w\right)\right)$$
19	14 15 18	cbvalv1	$$⊢\forall z\left(\left[z/x\right]\phi \leftrightarrow z=w\right)\leftrightarrow \forall y\left(\psi \leftrightarrow y=w\right)$$
20	11 19	bitri	$$⊢\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \forall y\left(\psi \leftrightarrow y=w\right)$$
21	20	abbii	$$⊢\left\{w|\forall x\left(\phi \leftrightarrow x=w\right)\right\}=\left\{w|\forall y\left(\psi \leftrightarrow y=w\right)\right\}$$
22	21	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\}$$
23		dfiota2	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{w|\forall x\left(\phi \leftrightarrow x=w\right)\right\}$$
24		dfiota2	$$⊢\left(\iota y|\psi \right)=\bigcup \left\{w|\forall y\left(\psi \leftrightarrow y=w\right)\right\}$$
25	22 23 24	3eqtr4i	$$⊢\left(\iota x|\phi \right)=\left(\iota y|\psi \right)$$