Theorem rabasiun 4324

Description: A class abstraction with a restricted existential quantification expressed as indexed union. (Contributed by Alexander van der Vekens, 29-Jul-2018.)

Assertion

Ref	Expression
rabasiun	|- { x e. X | E. y e. Y ph } = U_ y e. Y { x e. X | ph }

Distinct variable groups:   x, X, y   x, Y, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem rabasiun

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcv 2624	. . . . . 6 |- F/_ z X
2	1	nfcri 2617	. . . . 5 |- F/ z x e. X
3		nfv 1678	. . . . 5 |- F/ z E. y e. Y ph
4	2, 3	nfan 1870	. . . 4 |- F/ z ( x e. X /\ E. y e. Y ph )
5		nfcv 2624	. . . . . 6 |- F/_ x X
6	5	nfcri 2617	. . . . 5 |- F/ x z e. X
7		nfcv 2624	. . . . . 6 |- F/_ x Y
8		nfs1v 2159	. . . . . 6 |- F/ x [ z / x ] ph
9	7, 8	nfrex 2922	. . . . 5 |- F/ x E. y e. Y [ z / x ] ph
10	6, 9	nfan 1870	. . . 4 |- F/ x ( z e. X /\ E. y e. Y [ z / x ] ph )
11		eleq1 2534	. . . . 5 |- ( x = z -> ( x e. X <-> z e. X ) )
12		sbequ12 1956	. . . . . 6 |- ( x = z -> ( ph <-> [ z / x ] ph ) )
13	12	rexbidv 2968	. . . . 5 |- ( x = z -> ( E. y e. Y ph <-> E. y e. Y [ z / x ] ph ) )
14	11, 13	anbi12d 710	. . . 4 |- ( x = z -> ( ( x e. X /\ E. y e. Y ph ) <-> ( z e. X /\ E. y e. Y [ z / x ] ph ) ) )
15	4, 10, 14	cbvab 2603	. . 3 |- { x | ( x e. X /\ E. y e. Y ph ) } = { z | ( z e. X /\ E. y e. Y [ z / x ] ph ) }
16		r19.42v 3011	. . . . 5 |- ( E. y e. Y ( z e. X /\ [ z / x ] ph ) <-> ( z e. X /\ E. y e. Y [ z / x ] ph ) )
17		nfcv 2624	. . . . . . . 8 |- F/_ x z
18	17, 5, 8, 12	elrabf 3254	. . . . . . 7 |- ( z e. { x e. X | ph } <-> ( z e. X /\ [ z / x ] ph ) )
19	18	bicomi 202	. . . . . 6 |- ( ( z e. X /\ [ z / x ] ph ) <-> z e. { x e. X | ph } )
20	19	rexbii 2960	. . . . 5 |- ( E. y e. Y ( z e. X /\ [ z / x ] ph ) <-> E. y e. Y z e. { x e. X | ph } )
21	16, 20	bitr3i 251	. . . 4 |- ( ( z e. X /\ E. y e. Y [ z / x ] ph ) <-> E. y e. Y z e. { x e. X | ph } )
22	21	abbii 2596	. . 3 |- { z | ( z e. X /\ E. y e. Y [ z / x ] ph ) } = { z | E. y e. Y z e. { x e. X | ph } }
23	15, 22	eqtri 2491	. 2 |- { x | ( x e. X /\ E. y e. Y ph ) } = { z | E. y e. Y z e. { x e. X | ph } }
24		df-rab 2818	. 2 |- { x e. X | E. y e. Y ph } = { x | ( x e. X /\ E. y e. Y ph ) }
25		df-iun 4322	. 2 |- U_ y e. Y { x e. X | ph } = { z | E. y e. Y z e. { x e. X | ph } }
26	23, 24, 25	3eqtr4i 2501	1 |- { x e. X | E. y e. Y ph } = U_ y e. Y { x e. X | ph }

Syntax hints:   /\ wa 369   = wceq 1374   [wsb 1706   e. wcel 1762   {cab 2447   E.wrex 2810   {crab 2813   U_ciun 4320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-iun 4322

This theorem is referenced by:  hashrabrex  13588