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

Metamath Proof Explorer

Theorem iunin2

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)

Ref Expression
Assertion iunin2 ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
2 elin ⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
3 2 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
4 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
5 4 anbi2i ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
6 1 3 5 3bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
7 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
8 elin ⊢ ( 𝑦 ∈ ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
9 6 7 8 3bitr4i ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
10 9 eqriv ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶 )