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)

	Ref	Expression
Assertion	inuni	⊢ ( ∪ 𝐴 ∩ 𝐵 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) }

Proof

Step	Hyp	Ref	Expression
1		eluni2	⊢ ( 𝑧 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 )
2	1	anbi1i	⊢ ( ( 𝑧 ∈ ∪ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) )
3		elin	⊢ ( 𝑧 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ↔ ( 𝑧 ∈ ∪ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
4		ancom	⊢ ( ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) )
5		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) )
6	4 5	bitr4i	⊢ ( ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) )
8		rexcom4	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) )
9	7 8	bitr4i	⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) )
10		vex	⊢ 𝑦 ∈ V
11	10	inex1	⊢ ( 𝑦 ∩ 𝐵 ) ∈ V
12		eleq2	⊢ ( 𝑥 = ( 𝑦 ∩ 𝐵 ) → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ ( 𝑦 ∩ 𝐵 ) ) )
13	11 12	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) ↔ 𝑧 ∈ ( 𝑦 ∩ 𝐵 ) )
14		elin	⊢ ( 𝑧 ∈ ( 𝑦 ∩ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) )
15	13 14	bitri	⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) )
16	15	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) )
17		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) )
18	16 17	bitri	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝑥 = ( 𝑦 ∩ 𝐵 ) ∧ 𝑧 ∈ 𝑥 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) )
19	9 18	bitri	⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵 ) )
20	2 3 19	3bitr4i	⊢ ( 𝑧 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ) )
21		eluniab	⊢ ( 𝑧 ∈ ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) } ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) ) )
22	20 21	bitr4i	⊢ ( 𝑧 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ↔ 𝑧 ∈ ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) } )
23	22	eqriv	⊢ ( ∪ 𝐴 ∩ 𝐵 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) }