# Metamath Proof Explorer

## Theorem uni0b

Description: The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004)

Ref Expression
Assertion uni0b ${⊢}\bigcup {A}=\varnothing ↔{A}\subseteq \left\{\varnothing \right\}$

### Proof

Step Hyp Ref Expression
1 velsn ${⊢}{x}\in \left\{\varnothing \right\}↔{x}=\varnothing$
2 1 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in \left\{\varnothing \right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}=\varnothing$
3 dfss3 ${⊢}{A}\subseteq \left\{\varnothing \right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in \left\{\varnothing \right\}$
4 neq0 ${⊢}¬\bigcup {A}=\varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in \bigcup {A}$
5 rexcom4 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
6 neq0 ${⊢}¬{x}=\varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
7 6 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}=\varnothing ↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
8 eluni2 ${⊢}{y}\in \bigcup {A}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
9 8 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in \bigcup {A}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
10 5 7 9 3bitr4ri ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in \bigcup {A}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}=\varnothing$
11 rexnal ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}=\varnothing ↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}=\varnothing$
12 4 10 11 3bitri ${⊢}¬\bigcup {A}=\varnothing ↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}=\varnothing$
13 12 con4bii ${⊢}\bigcup {A}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}=\varnothing$
14 2 3 13 3bitr4ri ${⊢}\bigcup {A}=\varnothing ↔{A}\subseteq \left\{\varnothing \right\}$