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

Metamath Proof Explorer

Theorem iinin2

Description: Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	iinin2	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) ) )
2		elin	⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
4		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
5	4	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
6	5	anbi2i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
7	1 3 6	3bitr4g	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) ) )
8		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
9	8	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
10		elin	⊢ ( 𝑦 ∈ ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
11	7 9 10	3bitr4g	⊢ ( 𝐴 ≠ ∅ → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 ) ) )
12	11	eqrdv	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 ) )