Theorem iinuni

Description: A relationship involving union and indexed intersection. Exercise 23 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

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

Proof

Step	Hyp	Ref	Expression
1		r19.32v	|- ( A. x e. B ( y e. A \/ y e. x ) <-> ( y e. A \/ A. x e. B y e. x ) )
2		elun	|- ( y e. ( A u. x ) <-> ( y e. A \/ y e. x ) )
3	2	ralbii	|- ( A. x e. B y e. ( A u. x ) <-> A. x e. B ( y e. A \/ y e. x ) )
4		vex	|- y e. _V
5	4	elint2	|- ( y e. |^| B <-> A. x e. B y e. x )
6	5	orbi2i	|- ( ( y e. A \/ y e. |^| B ) <-> ( y e. A \/ A. x e. B y e. x ) )
7	1 3 6	3bitr4ri	|- ( ( y e. A \/ y e. |^| B ) <-> A. x e. B y e. ( A u. x ) )
8	7	abbii	|- { y | ( y e. A \/ y e. |^| B ) } = { y | A. x e. B y e. ( A u. x ) }
9		df-un	|- ( A u. |^| B ) = { y | ( y e. A \/ y e. |^| B ) }
10		df-iin	|- |^|_ x e. B ( A u. x ) = { y | A. x e. B y e. ( A u. x ) }
11	8 9 10	3eqtr4i	|- ( A u. |^| B ) = |^|_ x e. B ( A u. x )