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	⊢ ( ∪ 𝐴 ∩ 𝐵 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 ∩ 𝐵 ) }

Proof

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

Metamath Proof Explorer

Theorem inuni

Proof