Theorem csbriota 6166

Description: Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.)

Assertion

Ref	Expression
csbriota	|- [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph )

Distinct variable groups:   y, A   x, B   x, y

Allowed substitution hints:   ph( x, y)   A( x)   B( y)

Proof of Theorem csbriota

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbeq1 3392	. . . 4 |- ( z = A -> [_ z / x ]_ ( iota_ y e. B ph ) = [_ A / x ]_ ( iota_ y e. B ph ) )
2		dfsbcq2 3290	. . . . 5 |- ( z = A -> ( [ z / x ] ph <-> [. A / x ]. ph ) )
3	2	riotabidv 6156	. . . 4 |- ( z = A -> ( iota_ y e. B [ z / x ] ph ) = ( iota_ y e. B [. A / x ]. ph ) )
4	1, 3	eqeq12d 2473	. . 3 |- ( z = A -> ( [_ z / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [ z / x ] ph ) <-> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) ) )
5		vex 3074	. . . 4 |- z e. _V
6		nfs1v 2149	. . . . 5 |- F/ x [ z / x ] ph
7		nfcv 2613	. . . . 5 |- F/_ x B
8	6, 7	nfriota 6163	. . . 4 |- F/_ x ( iota_ y e. B [ z / x ] ph )
9		sbequ12 1945	. . . . 5 |- ( x = z -> ( ph <-> [ z / x ] ph ) )
10	9	riotabidv 6156	. . . 4 |- ( x = z -> ( iota_ y e. B ph ) = ( iota_ y e. B [ z / x ] ph ) )
11	5, 8, 10	csbief 3414	. . 3 |- [_ z / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [ z / x ] ph )
12	4, 11	vtoclg 3129	. 2 |- ( A e. _V -> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) )
13		csbprc 3774	. . 3 |- ( -. A e. _V -> [_ A / x ]_ ( iota_ y e. B ph ) = (/) )
14		df-riota 6154	. . . 4 |- ( iota_ y e. B [. A / x ]. ph ) = ( iota y ( y e. B /\ [. A / x ]. ph ) )
15		euex 2288	. . . . . . 7 |- ( E! y ( y e. B /\ [. A / x ]. ph ) -> E. y ( y e. B /\ [. A / x ]. ph ) )
16		sbcex 3297	. . . . . . . . 9 |- ( [. A / x ]. ph -> A e. _V )
17	16	adantl 466	. . . . . . . 8 |- ( ( y e. B /\ [. A / x ]. ph ) -> A e. _V )
18	17	exlimiv 1689	. . . . . . 7 |- ( E. y ( y e. B /\ [. A / x ]. ph ) -> A e. _V )
19	15, 18	syl 16	. . . . . 6 |- ( E! y ( y e. B /\ [. A / x ]. ph ) -> A e. _V )
20	19	con3i 135	. . . . 5 |- ( -. A e. _V -> -. E! y ( y e. B /\ [. A / x ]. ph ) )
21		iotanul 5497	. . . . 5 |- ( -. E! y ( y e. B /\ [. A / x ]. ph ) -> ( iota y ( y e. B /\ [. A / x ]. ph ) ) = (/) )
22	20, 21	syl 16	. . . 4 |- ( -. A e. _V -> ( iota y ( y e. B /\ [. A / x ]. ph ) ) = (/) )
23	14, 22	syl5req 2505	. . 3 |- ( -. A e. _V -> (/) = ( iota_ y e. B [. A / x ]. ph ) )
24	13, 23	eqtrd 2492	. 2 |- ( -. A e. _V -> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) )
25	12, 24	pm2.61i 164	1 |- [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph )

Syntax hints:   -. wn 3   /\ wa 369   = wceq 1370   E.wex 1587   [wsb 1702   e. wcel 1758   E!weu 2260   _Vcvv 3071   [.wsbc 3287   [_csb 3389   (/)c0 3738   iotacio 5480   iota_crio 6153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-in 3436  df-ss 3443  df-nul 3739  df-sn 3979  df-uni 4193  df-iota 5482  df-riota 6154

This theorem is referenced by:  csbriotagOLD  6167  cdlemkid3N  34886  cdlemkid4  34887