Theorem iunab

Description: The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\phi \right\}$$
3	1 2	nfiun	$$⊢\underset{\_}{Ⅎ}y\bigcup _{x\in A}\left\{y|\phi \right\}$$
4		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\exists x\in A\phi \right\}$$
5		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
6	5	rexbii	$$⊢\exists x\in Ay\in \left\{y|\phi \right\}\leftrightarrow \exists x\in A\phi$$
7		eliun	$$⊢y\in \bigcup _{x\in A}\left\{y|\phi \right\}\leftrightarrow \exists x\in Ay\in \left\{y|\phi \right\}$$
8		abid	$$⊢y\in \left\{y|\exists x\in A\phi \right\}\leftrightarrow \exists x\in A\phi$$
9	6 7 8	3bitr4i	$$⊢y\in \bigcup _{x\in A}\left\{y|\phi \right\}\leftrightarrow y\in \left\{y|\exists x\in A\phi \right\}$$
10	3 4 9	eqri	$$⊢\bigcup _{x\in A}\left\{y|\phi \right\}=\left\{y|\exists x\in A\phi \right\}$$