Theorem cbvriota

Description: Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvriotaw when possible. (Contributed by NM, 18-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvriota.1	|- F/ y ph
2		cbvriota.2	|- F/ x ps
3		cbvriota.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	cbviota	|- ( 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		sbequ	|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
14	2 3	sbie	|- ( [ y / x ] ph <-> ps )
15	13 14	bitrdi	|- ( z = y -> ( [ z / x ] ph <-> ps ) )
16	12 15	anbi12d	|- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
17		nfv	|- F/ y z e. A
18	1	nfsb	|- F/ y [ z / x ] ph
19	17 18	nfan	|- F/ y ( z e. A /\ [ z / x ] ph )
20		nfv	|- F/ z ( y e. A /\ ps )
21	16 19 20	cbviota	|- ( iota z ( z e. A /\ [ z / x ] ph ) ) = ( iota y ( y e. A /\ ps ) )
22	11 21	eqtri	|- ( iota x ( x e. A /\ ph ) ) = ( iota y ( y e. A /\ ps ) )
23		df-riota	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
24		df-riota	|- ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) )
25	22 23 24	3eqtr4i	|- ( iota_ x e. A ph ) = ( iota_ y e. A ps )