Theorem iuncom4

Description: Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014)

	Ref	Expression
Assertion	iuncom4	|- U_ x e. A U. B = U. U_ x e. A B

Proof

Step	Hyp	Ref	Expression
1		df-rex	|- ( E. z e. B y e. z <-> E. z ( z e. B /\ y e. z ) )
2	1	rexbii	|- ( E. x e. A E. z e. B y e. z <-> E. x e. A E. z ( z e. B /\ y e. z ) )
3		rexcom4	|- ( E. x e. A E. z ( z e. B /\ y e. z ) <-> E. z E. x e. A ( z e. B /\ y e. z ) )
4	2 3	bitri	|- ( E. x e. A E. z e. B y e. z <-> E. z E. x e. A ( z e. B /\ y e. z ) )
5		r19.41v	|- ( E. x e. A ( z e. B /\ y e. z ) <-> ( E. x e. A z e. B /\ y e. z ) )
6	5	exbii	|- ( E. z E. x e. A ( z e. B /\ y e. z ) <-> E. z ( E. x e. A z e. B /\ y e. z ) )
7	4 6	bitri	|- ( E. x e. A E. z e. B y e. z <-> E. z ( E. x e. A z e. B /\ y e. z ) )
8		eluni2	|- ( y e. U. B <-> E. z e. B y e. z )
9	8	rexbii	|- ( E. x e. A y e. U. B <-> E. x e. A E. z e. B y e. z )
10		df-rex	|- ( E. z e. U_ x e. A B y e. z <-> E. z ( z e. U_ x e. A B /\ y e. z ) )
11		eliun	|- ( z e. U_ x e. A B <-> E. x e. A z e. B )
12	11	anbi1i	|- ( ( z e. U_ x e. A B /\ y e. z ) <-> ( E. x e. A z e. B /\ y e. z ) )
13	12	exbii	|- ( E. z ( z e. U_ x e. A B /\ y e. z ) <-> E. z ( E. x e. A z e. B /\ y e. z ) )
14	10 13	bitri	|- ( E. z e. U_ x e. A B y e. z <-> E. z ( E. x e. A z e. B /\ y e. z ) )
15	7 9 14	3bitr4i	|- ( E. x e. A y e. U. B <-> E. z e. U_ x e. A B y e. z )
16		eliun	|- ( y e. U_ x e. A U. B <-> E. x e. A y e. U. B )
17		eluni2	|- ( y e. U. U_ x e. A B <-> E. z e. U_ x e. A B y e. z )
18	15 16 17	3bitr4i	|- ( y e. U_ x e. A U. B <-> y e. U. U_ x e. A B )
19	18	eqriv	|- U_ x e. A U. B = U. U_ x e. A B