Theorem rabasiun 4295

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 2602	. . . . . 6 |- F/_ z X
2	1	nfcri 2596	. . . . 5 |- F/ z x e. X
3		nfv 1771	. . . . 5 |- F/ z E. y e. Y ph
4	2, 3	nfan 2021	. . . 4 |- F/ z ( x e. X /\ E. y e. Y ph )
5		nfcv 2602	. . . . . 6 |- F/_ x X
6	5	nfcri 2596	. . . . 5 |- F/ x z e. X
7		nfcv 2602	. . . . . 6 |- F/_ x Y
8		nfs1v 2276	. . . . . 6 |- F/ x [ z / x ] ph
9	7, 8	nfrex 2861	. . . . 5 |- F/ x E. y e. Y [ z / x ] ph
10	6, 9	nfan 2021	. . . 4 |- F/ x ( z e. X /\ E. y e. Y [ z / x ] ph )
11		eleq1 2527	. . . . 5 |- ( x = z -> ( x e. X <-> z e. X ) )
12		sbequ12 2093	. . . . . 6 |- ( x = z -> ( ph <-> [ z / x ] ph ) )
13	12	rexbidv 2912	. . . . 5 |- ( x = z -> ( E. y e. Y ph <-> E. y e. Y [ z / x ] ph ) )
14	11, 13	anbi12d 722	. . . 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 2584	. . 3 |- { x | ( x e. X /\ E. y e. Y ph ) } = { z | ( z e. X /\ E. y e. Y [ z / x ] ph ) }
16		r19.42v 2956	. . . . 5 |- ( E. y e. Y ( z e. X /\ [ z / x ] ph ) <-> ( z e. X /\ E. y e. Y [ z / x ] ph ) )
17		nfcv 2602	. . . . . . . 8 |- F/_ x z
18	17, 5, 8, 12	elrabf 3205	. . . . . . 7 |- ( z e. { x e. X | ph } <-> ( z e. X /\ [ z / x ] ph ) )
19	18	bicomi 207	. . . . . 6 |- ( ( z e. X /\ [ z / x ] ph ) <-> z e. { x e. X | ph } )
20	19	rexbii 2900	. . . . 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 259	. . . 4 |- ( ( z e. X /\ E. y e. Y [ z / x ] ph ) <-> E. y e. Y z e. { x e. X | ph } )
22	21	abbii 2577	. . 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 2483	. 2 |- { x | ( x e. X /\ E. y e. Y ph ) } = { z | E. y e. Y z e. { x e. X | ph } }
24		df-rab 2757	. 2 |- { x e. X | E. y e. Y ph } = { x | ( x e. X /\ E. y e. Y ph ) }
25		df-iun 4293	. 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 2493	1 |- { x e. X | E. y e. Y ph } = U_ y e. Y { x e. X | ph }

Syntax hints:   /\ wa 375   = wceq 1454   [wsb 1807   e. wcel 1897   {cab 2447   E.wrex 2749   {crab 2752   U_ciun 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-iun 4293

This theorem is referenced by:  hashrabrex  13931