Theorem eliun

Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003)

	Ref	Expression
Assertion	eliun	$$⊢A\in \bigcup _{x\in B}C\leftrightarrow \exists x\in BA\in C$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \bigcup _{x\in B}C\to A\in \mathrm{V}$$
2		elex	$$⊢A\in C\to A\in \mathrm{V}$$
3	2	rexlimivw	$$⊢\exists x\in BA\in C\to A\in \mathrm{V}$$
4		eleq1	$$⊢y=A\to \left(y\in C\leftrightarrow A\in C\right)$$
5	4	rexbidv	$$⊢y=A\to \left(\exists x\in By\in C\leftrightarrow \exists x\in BA\in C\right)$$
6		df-iun	$$⊢\bigcup _{x\in B}C=\left\{y|\exists x\in By\in C\right\}$$
7	5 6	elab2g	$$⊢A\in \mathrm{V}\to \left(A\in \bigcup _{x\in B}C\leftrightarrow \exists x\in BA\in C\right)$$
8	1 3 7	pm5.21nii	$$⊢A\in \bigcup _{x\in B}C\leftrightarrow \exists x\in BA\in C$$