# 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 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
Assertion iunin1f ${⊢}\bigcup _{{x}\in {A}}\left({B}\cap {C}\right)=\bigcup _{{x}\in {A}}{B}\cap {C}$

### Proof

Step Hyp Ref Expression
1 iunin1f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
2 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {C}$
3 2 r19.41 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {y}\in {C}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\wedge {y}\in {C}\right)$
4 elin ${⊢}{y}\in \left({B}\cap {C}\right)↔\left({y}\in {B}\wedge {y}\in {C}\right)$
5 4 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left({B}\cap {C}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {y}\in {C}\right)$
6 eliun ${⊢}{y}\in \bigcup _{{x}\in {A}}{B}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
7 6 anbi1i ${⊢}\left({y}\in \bigcup _{{x}\in {A}}{B}\wedge {y}\in {C}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\wedge {y}\in {C}\right)$
8 3 5 7 3bitr4i ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left({B}\cap {C}\right)↔\left({y}\in \bigcup _{{x}\in {A}}{B}\wedge {y}\in {C}\right)$
9 eliun ${⊢}{y}\in \bigcup _{{x}\in {A}}\left({B}\cap {C}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left({B}\cap {C}\right)$
10 elin ${⊢}{y}\in \left(\bigcup _{{x}\in {A}}{B}\cap {C}\right)↔\left({y}\in \bigcup _{{x}\in {A}}{B}\wedge {y}\in {C}\right)$
11 8 9 10 3bitr4i ${⊢}{y}\in \bigcup _{{x}\in {A}}\left({B}\cap {C}\right)↔{y}\in \left(\bigcup _{{x}\in {A}}{B}\cap {C}\right)$
12 11 eqriv ${⊢}\bigcup _{{x}\in {A}}\left({B}\cap {C}\right)=\bigcup _{{x}\in {A}}{B}\cap {C}$