# Metamath Proof Explorer

## Theorem uniun

Description: The class union of the union of two classes. Theorem 8.3 of Quine p. 53. (Contributed by NM, 20-Aug-1993)

Ref Expression
Assertion uniun ${⊢}\bigcup \left({A}\cup {B}\right)=\bigcup {A}\cup \bigcup {B}$

### Proof

Step Hyp Ref Expression
1 19.43 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {y}\wedge {y}\in {A}\right)\vee \left({x}\in {y}\wedge {y}\in {B}\right)\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {A}\right)\vee \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {B}\right)\right)$
2 elun ${⊢}{y}\in \left({A}\cup {B}\right)↔\left({y}\in {A}\vee {y}\in {B}\right)$
3 2 anbi2i ${⊢}\left({x}\in {y}\wedge {y}\in \left({A}\cup {B}\right)\right)↔\left({x}\in {y}\wedge \left({y}\in {A}\vee {y}\in {B}\right)\right)$
4 andi ${⊢}\left({x}\in {y}\wedge \left({y}\in {A}\vee {y}\in {B}\right)\right)↔\left(\left({x}\in {y}\wedge {y}\in {A}\right)\vee \left({x}\in {y}\wedge {y}\in {B}\right)\right)$
5 3 4 bitri ${⊢}\left({x}\in {y}\wedge {y}\in \left({A}\cup {B}\right)\right)↔\left(\left({x}\in {y}\wedge {y}\in {A}\right)\vee \left({x}\in {y}\wedge {y}\in {B}\right)\right)$
6 5 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in \left({A}\cup {B}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {y}\wedge {y}\in {A}\right)\vee \left({x}\in {y}\wedge {y}\in {B}\right)\right)$
7 eluni ${⊢}{x}\in \bigcup {A}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {A}\right)$
8 eluni ${⊢}{x}\in \bigcup {B}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {B}\right)$
9 7 8 orbi12i ${⊢}\left({x}\in \bigcup {A}\vee {x}\in \bigcup {B}\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {A}\right)\vee \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {B}\right)\right)$
10 1 6 9 3bitr4i ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in \left({A}\cup {B}\right)\right)↔\left({x}\in \bigcup {A}\vee {x}\in \bigcup {B}\right)$
11 eluni ${⊢}{x}\in \bigcup \left({A}\cup {B}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in \left({A}\cup {B}\right)\right)$
12 elun ${⊢}{x}\in \left(\bigcup {A}\cup \bigcup {B}\right)↔\left({x}\in \bigcup {A}\vee {x}\in \bigcup {B}\right)$
13 10 11 12 3bitr4i ${⊢}{x}\in \bigcup \left({A}\cup {B}\right)↔{x}\in \left(\bigcup {A}\cup \bigcup {B}\right)$
14 13 eqriv ${⊢}\bigcup \left({A}\cup {B}\right)=\bigcup {A}\cup \bigcup {B}$