Theorem cbvriotaw

Description: Change bound variable in a restricted description binder. Version of cbvriota with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 18-Mar-2013) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Hypotheses	cbvriotaw.1	|- F/ y ph
	cbvriotaw.2	|- F/ x ps
	cbvriotaw.3	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvriotaw	|- ( iota_ x e. A ph ) = ( iota_ y e. A ps )

Proof

Step	Hyp	Ref	Expression
1		cbvriotaw.1	|- F/ y ph
2		cbvriotaw.2	|- F/ x ps
3		cbvriotaw.3	|- ( x = y -> ( ph <-> ps ) )
4		eleq1w	|- ( x = z -> ( x e. A <-> z e. A ) )
5		sbequ12	|- ( x = z -> ( ph <-> [ z / x ] ph ) )
6	4 5	anbi12d	|- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
7		nfv	|- F/ z ( x e. A /\ ph )
8		nfv	|- F/ x z e. A
9		nfs1v	|- F/ x [ z / x ] ph
10	8 9	nfan	|- F/ x ( z e. A /\ [ z / x ] ph )
11	6 7 10	cbviotaw	|- ( iota x ( x e. A /\ ph ) ) = ( iota z ( z e. A /\ [ z / x ] ph ) )
12		eleq1w	|- ( z = y -> ( z e. A <-> y e. A ) )
13	2 3	sbhypf	|- ( z = y -> ( [ z / x ] ph <-> ps ) )
14	12 13	anbi12d	|- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
15		nfv	|- F/ y z e. A
16	1	nfsbv	|- F/ y [ z / x ] ph
17	15 16	nfan	|- F/ y ( z e. A /\ [ z / x ] ph )
18		nfv	|- F/ z ( y e. A /\ ps )
19	14 17 18	cbviotaw	|- ( iota z ( z e. A /\ [ z / x ] ph ) ) = ( iota y ( y e. A /\ ps ) )
20	11 19	eqtri	|- ( iota x ( x e. A /\ ph ) ) = ( iota y ( y e. A /\ ps ) )
21		df-riota	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
22		df-riota	|- ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) )
23	20 21 22	3eqtr4i	|- ( iota_ x e. A ph ) = ( iota_ y e. A ps )