Theorem iinun2

Description: Indexed intersection of union. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004)

	Ref	Expression
Assertion	iinun2	|- |^|_ x e. A ( B u. C ) = ( B u. |^|_ x e. A C )

Proof

Step	Hyp	Ref	Expression
1		r19.32v	|- ( A. x e. A ( y e. B \/ y e. C ) <-> ( y e. B \/ A. x e. A y e. C ) )
2		elun	|- ( y e. ( B u. C ) <-> ( y e. B \/ y e. C ) )
3	2	ralbii	|- ( A. x e. A y e. ( B u. C ) <-> A. x e. A ( y e. B \/ y e. C ) )
4		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A C <-> A. x e. A y e. C ) )
5	4	elv	|- ( y e. |^|_ x e. A C <-> A. x e. A y e. C )
6	5	orbi2i	|- ( ( y e. B \/ y e. |^|_ x e. A C ) <-> ( y e. B \/ A. x e. A y e. C ) )
7	1 3 6	3bitr4i	|- ( A. x e. A y e. ( B u. C ) <-> ( y e. B \/ y e. |^|_ x e. A C ) )
8		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A ( B u. C ) <-> A. x e. A y e. ( B u. C ) ) )
9	8	elv	|- ( y e. |^|_ x e. A ( B u. C ) <-> A. x e. A y e. ( B u. C ) )
10		elun	|- ( y e. ( B u. |^|_ x e. A C ) <-> ( y e. B \/ y e. |^|_ x e. A C ) )
11	7 9 10	3bitr4i	|- ( y e. |^|_ x e. A ( B u. C ) <-> y e. ( B u. |^|_ x e. A C ) )
12	11	eqriv	|- |^|_ x e. A ( B u. C ) = ( B u. |^|_ x e. A C )