Theorem eliun

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

	Ref	Expression
Assertion	eliun	|- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. U_ x e. B C -> A e. _V )
2		elex	|- ( A e. C -> A e. _V )
3	2	rexlimivw	|- ( E. x e. B A e. C -> A e. _V )
4		eleq1	|- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv	|- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun	|- U_ x e. B C = { y | E. x e. B y e. C }
7	5 6	elab2g	|- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1 3 7	pm5.21nii	|- ( A e. U_ x e. B C <-> E. x e. B A e. C )