Theorem sb8iota

Description: Variable substitution in description binder. Compare sb8eu . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 18-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sb8iota.1	|- F/ y ph
Assertion	sb8iota	|- ( iota x ph ) = ( iota y [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		sb8iota.1	|- F/ y ph
2		nfv	|- F/ w ( ph <-> x = z )
3	2	sb8	|- ( A. x ( ph <-> x = z ) <-> A. w [ w / x ] ( ph <-> x = z ) )
4		sbbi	|- ( [ w / x ] ( ph <-> x = z ) <-> ( [ w / x ] ph <-> [ w / x ] x = z ) )
5	1	nfsb	|- F/ y [ w / x ] ph
6		equsb3	|- ( [ w / x ] x = z <-> w = z )
7		nfv	|- F/ y w = z
8	6 7	nfxfr	|- F/ y [ w / x ] x = z
9	5 8	nfbi	|- F/ y ( [ w / x ] ph <-> [ w / x ] x = z )
10	4 9	nfxfr	|- F/ y [ w / x ] ( ph <-> x = z )
11		nfv	|- F/ w [ y / x ] ( ph <-> x = z )
12		sbequ	|- ( w = y -> ( [ w / x ] ( ph <-> x = z ) <-> [ y / x ] ( ph <-> x = z ) ) )
13	10 11 12	cbvalv1	|- ( A. w [ w / x ] ( ph <-> x = z ) <-> A. y [ y / x ] ( ph <-> x = z ) )
14		equsb3	|- ( [ y / x ] x = z <-> y = z )
15	14	sblbis	|- ( [ y / x ] ( ph <-> x = z ) <-> ( [ y / x ] ph <-> y = z ) )
16	15	albii	|- ( A. y [ y / x ] ( ph <-> x = z ) <-> A. y ( [ y / x ] ph <-> y = z ) )
17	3 13 16	3bitri	|- ( A. x ( ph <-> x = z ) <-> A. y ( [ y / x ] ph <-> y = z ) )
18	17	abbii	|- { z | A. x ( ph <-> x = z ) } = { z | A. y ( [ y / x ] ph <-> y = z ) }
19	18	unieqi	|- U. { z | A. x ( ph <-> x = z ) } = U. { z | A. y ( [ y / x ] ph <-> y = z ) }
20		dfiota2	|- ( iota x ph ) = U. { z | A. x ( ph <-> x = z ) }
21		dfiota2	|- ( iota y [ y / x ] ph ) = U. { z | A. y ( [ y / x ] ph <-> y = z ) }
22	19 20 21	3eqtr4i	|- ( iota x ph ) = ( iota y [ y / x ] ph )