This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunin1f

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use uniiun to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004) (Revised by Thierry Arnoux, 2-May-2020)

		Ref	Expression
	Hypothesis	iunin1f.1	⊢ Ⅎ 𝑥 𝐶
	Assertion	iunin1f	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		iunin1f.1	⊢ Ⅎ 𝑥 𝐶
2	1	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐶
3	2	r19.41	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
4		elin	⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
5	4	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
6		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
7	6	anbi1i	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
8	3 5 7	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
9		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
10		elin	⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
11	8 9 10	3bitr4i	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) )
12	11	eqriv	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 )