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	3 4	cleqf	$$⊢\bigcup _{x\in A}\left\{y|\phi \right\}=\left\{y|\exists x\in A\phi \right\}\leftrightarrow \forall y\left(y\in \bigcup _{x\in A}\left\{y|\phi \right\}\leftrightarrow y\in \left\{y|\exists x\in A\phi \right\}\right)$$
6		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
7	6	rexbii	$$⊢\exists x\in Ay\in \left\{y|\phi \right\}\leftrightarrow \exists x\in A\phi$$
8		eliun	$$⊢y\in \bigcup _{x\in A}\left\{y|\phi \right\}\leftrightarrow \exists x\in Ay\in \left\{y|\phi \right\}$$
9		abid	$$⊢y\in \left\{y|\exists x\in A\phi \right\}\leftrightarrow \exists x\in A\phi$$
10	7 8 9	3bitr4i	$$⊢y\in \bigcup _{x\in A}\left\{y|\phi \right\}\leftrightarrow y\in \left\{y|\exists x\in A\phi \right\}$$
11	5 10	mpgbir	$$⊢\bigcup _{x\in A}\left\{y|\phi \right\}=\left\{y|\exists x\in A\phi \right\}$$