Theorem iunrab

Description: The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004) (Proof shortened by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	iunrab	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}=\left\{y\in B|\exists x\in A\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		iunab	$$⊢\bigcup _{x\in A}\left\{y|\left(y\in B\wedge \phi \right)\right\}=\left\{y|\exists x\in A\left(y\in B\wedge \phi \right)\right\}$$
2		df-rab	$$⊢\left\{y\in B|\phi \right\}=\left\{y|\left(y\in B\wedge \phi \right)\right\}$$
3	2	a1i	$$⊢x\in A\to \left\{y\in B|\phi \right\}=\left\{y|\left(y\in B\wedge \phi \right)\right\}$$
4	3	iuneq2i	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}=\bigcup _{x\in A}\left\{y|\left(y\in B\wedge \phi \right)\right\}$$
5		df-rab	$$⊢\left\{y\in B|\exists x\in A\phi \right\}=\left\{y|\left(y\in B\wedge \exists x\in A\phi \right)\right\}$$
6		r19.42v	$$⊢\exists x\in A\left(y\in B\wedge \phi \right)\leftrightarrow \left(y\in B\wedge \exists x\in A\phi \right)$$
7	6	abbii	$$⊢\left\{y|\exists x\in A\left(y\in B\wedge \phi \right)\right\}=\left\{y|\left(y\in B\wedge \exists x\in A\phi \right)\right\}$$
8	5 7	eqtr4i	$$⊢\left\{y\in B|\exists x\in A\phi \right\}=\left\{y|\exists x\in A\left(y\in B\wedge \phi \right)\right\}$$
9	1 4 8	3eqtr4i	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}=\left\{y\in B|\exists x\in A\phi \right\}$$