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) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Hypotheses	cbviotaw.1	|- ( x = y -> ( ph <-> ps ) )
	cbviotaw.2	|- F/ y ph
	cbviotaw.3	|- F/ x ps
Assertion	cbviotaw	|- ( iota x ph ) = ( iota y ps )

Proof

Step	Hyp	Ref	Expression
1		cbviotaw.1	|- ( x = y -> ( ph <-> ps ) )
2		cbviotaw.2	|- F/ y ph
3		cbviotaw.3	|- F/ x ps
4		nfv	|- F/ z ( ph <-> x = w )
5		nfs1v	|- F/ x [ z / x ] ph
6		nfv	|- F/ x z = w
7	5 6	nfbi	|- F/ x ( [ z / x ] ph <-> z = w )
8		sbequ12	|- ( x = z -> ( ph <-> [ z / x ] ph ) )
9		equequ1	|- ( x = z -> ( x = w <-> z = w ) )
10	8 9	bibi12d	|- ( x = z -> ( ( ph <-> x = w ) <-> ( [ z / x ] ph <-> z = w ) ) )
11	4 7 10	cbvalv1	|- ( A. x ( ph <-> x = w ) <-> A. z ( [ z / x ] ph <-> z = w ) )
12	2	nfsbv	|- F/ y [ z / x ] ph
13		nfv	|- F/ y z = w
14	12 13	nfbi	|- F/ y ( [ z / x ] ph <-> z = w )
15		nfv	|- F/ z ( ps <-> y = w )
16	3 1	sbhypf	|- ( z = y -> ( [ z / x ] ph <-> ps ) )
17		equequ1	|- ( z = y -> ( z = w <-> y = w ) )
18	16 17	bibi12d	|- ( z = y -> ( ( [ z / x ] ph <-> z = w ) <-> ( ps <-> y = w ) ) )
19	14 15 18	cbvalv1	|- ( A. z ( [ z / x ] ph <-> z = w ) <-> A. y ( ps <-> y = w ) )
20	11 19	bitri	|- ( A. x ( ph <-> x = w ) <-> A. y ( ps <-> y = w ) )
21	20	abbii	|- { w | A. x ( ph <-> x = w ) } = { w | A. y ( ps <-> y = w ) }
22	21	unieqi	|- U. { w | A. x ( ph <-> x = w ) } = U. { w | A. y ( ps <-> y = w ) }
23		dfiota2	|- ( iota x ph ) = U. { w | A. x ( ph <-> x = w ) }
24		dfiota2	|- ( iota y ps ) = U. { w | A. y ( ps <-> y = w ) }
25	22 23 24	3eqtr4i	|- ( iota x ph ) = ( iota y ps )