Theorem inuni

Description: The intersection of a union U. A with a class B is equal to the union of the intersections of each element of A with B . (Contributed by FL, 24-Mar-2007) (Proof shortened by Wolf Lammen, 15-May-2025)

	Ref	Expression
Assertion	inuni	|- ( U. A i^i B ) = U. { x | E. y e. A x = ( y i^i B ) }

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( z e. x /\ E. y e. A x = ( y i^i B ) ) <-> ( E. y e. A x = ( y i^i B ) /\ z e. x ) )
2		r19.41v	|- ( E. y e. A ( x = ( y i^i B ) /\ z e. x ) <-> ( E. y e. A x = ( y i^i B ) /\ z e. x ) )
3	1 2	bitr4i	|- ( ( z e. x /\ E. y e. A x = ( y i^i B ) ) <-> E. y e. A ( x = ( y i^i B ) /\ z e. x ) )
4	3	exbii	|- ( E. x ( z e. x /\ E. y e. A x = ( y i^i B ) ) <-> E. x E. y e. A ( x = ( y i^i B ) /\ z e. x ) )
5		eluniab	|- ( z e. U. { x | E. y e. A x = ( y i^i B ) } <-> E. x ( z e. x /\ E. y e. A x = ( y i^i B ) ) )
6		eluni2	|- ( z e. U. A <-> E. y e. A z e. y )
7	6	anbi1i	|- ( ( z e. U. A /\ z e. B ) <-> ( E. y e. A z e. y /\ z e. B ) )
8		elin	|- ( z e. ( U. A i^i B ) <-> ( z e. U. A /\ z e. B ) )
9		r19.41v	|- ( E. y e. A ( z e. y /\ z e. B ) <-> ( E. y e. A z e. y /\ z e. B ) )
10	7 8 9	3bitr4i	|- ( z e. ( U. A i^i B ) <-> E. y e. A ( z e. y /\ z e. B ) )
11		vex	|- y e. _V
12	11	inex1	|- ( y i^i B ) e. _V
13		eleq2	|- ( x = ( y i^i B ) -> ( z e. x <-> z e. ( y i^i B ) ) )
14	12 13	ceqsexv	|- ( E. x ( x = ( y i^i B ) /\ z e. x ) <-> z e. ( y i^i B ) )
15		elin	|- ( z e. ( y i^i B ) <-> ( z e. y /\ z e. B ) )
16	14 15	bitri	|- ( E. x ( x = ( y i^i B ) /\ z e. x ) <-> ( z e. y /\ z e. B ) )
17	16	rexbii	|- ( E. y e. A E. x ( x = ( y i^i B ) /\ z e. x ) <-> E. y e. A ( z e. y /\ z e. B ) )
18		rexcom4	|- ( E. y e. A E. x ( x = ( y i^i B ) /\ z e. x ) <-> E. x E. y e. A ( x = ( y i^i B ) /\ z e. x ) )
19	10 17 18	3bitr2i	|- ( z e. ( U. A i^i B ) <-> E. x E. y e. A ( x = ( y i^i B ) /\ z e. x ) )
20	4 5 19	3bitr4ri	|- ( z e. ( U. A i^i B ) <-> z e. U. { x | E. y e. A x = ( y i^i B ) } )
21	20	eqriv	|- ( U. A i^i B ) = U. { x | E. y e. A x = ( y i^i B ) }