Theorem coiun1

Description: Composition with an indexed union. Proof analgous to that of coiun . (Contributed by RP, 20-Jun-2020)

	Ref	Expression
Assertion	coiun1	|- ( U_ x e. C A o. B ) = U_ x e. C ( A o. B )

Proof

Step	Hyp	Ref	Expression
1		relco	|- Rel ( U_ x e. C A o. B )
2		reliun	|- ( Rel U_ x e. C ( A o. B ) <-> A. x e. C Rel ( A o. B ) )
3		relco	|- Rel ( A o. B )
4	3	a1i	|- ( x e. C -> Rel ( A o. B ) )
5	2 4	mprgbir	|- Rel U_ x e. C ( A o. B )
6		eliun	|- ( <. w , z >. e. U_ x e. C A <-> E. x e. C <. w , z >. e. A )
7		df-br	|- ( w U_ x e. C A z <-> <. w , z >. e. U_ x e. C A )
8		df-br	|- ( w A z <-> <. w , z >. e. A )
9	8	rexbii	|- ( E. x e. C w A z <-> E. x e. C <. w , z >. e. A )
10	6 7 9	3bitr4i	|- ( w U_ x e. C A z <-> E. x e. C w A z )
11	10	anbi2i	|- ( ( y B w /\ w U_ x e. C A z ) <-> ( y B w /\ E. x e. C w A z ) )
12		r19.42v	|- ( E. x e. C ( y B w /\ w A z ) <-> ( y B w /\ E. x e. C w A z ) )
13	11 12	bitr4i	|- ( ( y B w /\ w U_ x e. C A z ) <-> E. x e. C ( y B w /\ w A z ) )
14	13	exbii	|- ( E. w ( y B w /\ w U_ x e. C A z ) <-> E. w E. x e. C ( y B w /\ w A z ) )
15		rexcom4	|- ( E. x e. C E. w ( y B w /\ w A z ) <-> E. w E. x e. C ( y B w /\ w A z ) )
16	14 15	bitr4i	|- ( E. w ( y B w /\ w U_ x e. C A z ) <-> E. x e. C E. w ( y B w /\ w A z ) )
17		vex	|- y e. _V
18		vex	|- z e. _V
19	17 18	opelco	|- ( <. y , z >. e. ( U_ x e. C A o. B ) <-> E. w ( y B w /\ w U_ x e. C A z ) )
20		eliun	|- ( <. y , z >. e. U_ x e. C ( A o. B ) <-> E. x e. C <. y , z >. e. ( A o. B ) )
21	17 18	opelco	|- ( <. y , z >. e. ( A o. B ) <-> E. w ( y B w /\ w A z ) )
22	21	rexbii	|- ( E. x e. C <. y , z >. e. ( A o. B ) <-> E. x e. C E. w ( y B w /\ w A z ) )
23	20 22	bitri	|- ( <. y , z >. e. U_ x e. C ( A o. B ) <-> E. x e. C E. w ( y B w /\ w A z ) )
24	16 19 23	3bitr4i	|- ( <. y , z >. e. ( U_ x e. C A o. B ) <-> <. y , z >. e. U_ x e. C ( A o. B ) )
25	1 5 24	eqrelriiv	|- ( U_ x e. C A o. B ) = U_ x e. C ( A o. B )