Theorem iunrab 2586

Description: The indexed union of a restricted class abstraction.

Assertion

Ref	Expression
iunrab	|- U_x e. A {y e. B | ph} = {y e. B | E.x e. A ph}

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

Proof of Theorem iunrab

Step	Hyp	Ref	Expression
1		df-rab 1644	. 2 |- {z e. B | E.x e. A [z / y]ph} = {z | (z e. B /\ E.x e. A [z / y]ph)}
2		ax-17 968	. . 3 |- (x e. B -> A.y x e. B)
3		ax-17 968	. . 3 |- (x e. B -> A.z x e. B)
4		ax-17 968	. . 3 |- (E.x e. A ph -> A.zE.x e. A ph)
5		ax-17 968	. . . 4 |- (x e. A -> A.y x e. A)
6		hbs1 1327	. . . 4 |- ([z / y]ph -> A.y[z / y]ph)
7	5, 6	hbrex 1680	. . 3 |- (E.x e. A [z / y]ph -> A.yE.x e. A [z / y]ph)
8		sbequ12 1177	. . . 4 |- (y = z -> (ph <-> [z / y]ph))
9	8	rexbidv 1656	. . 3 |- (y = z -> (E.x e. A ph <-> E.x e. A [z / y]ph))
10	2, 3, 4, 7, 9	cbvrab 1901	. 2 |- {y e. B | E.x e. A ph} = {z e. B | E.x e. A [z / y]ph}
11		eliun 2560	. . . 4 |- (z e. U_x e. A {y e. B | ph} <-> E.x e. A z e. {y e. B | ph})
12	2	elrabsf 1953	. . . . 5 |- (z e. {y e. B | ph} <-> (z e. B /\ [z / y]ph))
13	12	rexbii 1660	. . . 4 |- (E.x e. A z e. {y e. B | ph} <-> E.x e. A (z e. B /\ [z / y]ph))
14		r19.42v 1756	. . . 4 |- (E.x e. A (z e. B /\ [z / y]ph) <-> (z e. B /\ E.x e. A [z / y]ph))
15	11, 13, 14	3bitr 177	. . 3 |- (z e. U_x e. A {y e. B | ph} <-> (z e. B /\ E.x e. A [z / y]ph))
16	15	abbi2i 1566	. 2 |- U_x e. A {y e. B | ph} = {z | (z e. B /\ E.x e. A [z / y]ph)}
17	1, 10, 16	3eqtr4r 1498	1 |- U_x e. A {y e. B | ph} = {y e. B | E.x e. A ph}

Syntax hints:   /\ wa 223   = wceq 953   e. wcel 955  [wsbc 1166  {cab 1456  E.wrex 1638  {crab 1640  U_ciun 2556

This theorem is referenced by:  iunab 2587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-rex 1642  df-rab 1644  df-v 1803  df-sbc 1932  df-iun 2558

Copyright terms: Public domain