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 ⊢ ⋃ A = ∅ ↔ A ⊆ ∅

Proof

Step Hyp Ref Expression
1 velsn ⊢ x ∈ ∅ ↔ x = ∅
2 1 ralbii ⊢ ∀ x ∈ A x ∈ ∅ ↔ ∀ x ∈ A x = ∅
3 dfss3 ⊢ A ⊆ ∅ ↔ ∀ x ∈ A x ∈ ∅
4 neq0 ⊢ ¬ ⋃ A = ∅ ↔ ∃ y y ∈ ⋃ A
5 rexcom4 ⊢ ∃ x ∈ A ∃ y y ∈ x ↔ ∃ y ∃ x ∈ A y ∈ x
6 neq0 ⊢ ¬ x = ∅ ↔ ∃ y y ∈ x
7 6 rexbii ⊢ ∃ x ∈ A ¬ x = ∅ ↔ ∃ x ∈ A ∃ y y ∈ x
8 eluni2 ⊢ y ∈ ⋃ A ↔ ∃ x ∈ A y ∈ x
9 8 exbii ⊢ ∃ y y ∈ ⋃ A ↔ ∃ y ∃ x ∈ A y ∈ x
10 5 7 9 3bitr4ri ⊢ ∃ y y ∈ ⋃ A ↔ ∃ x ∈ A ¬ x = ∅
11 rexnal ⊢ ∃ x ∈ A ¬ x = ∅ ↔ ¬ ∀ x ∈ A x = ∅
12 4 10 11 3bitri ⊢ ¬ ⋃ A = ∅ ↔ ¬ ∀ x ∈ A x = ∅
13 12 con4bii ⊢ ⋃ A = ∅ ↔ ∀ x ∈ A x = ∅
14 2 3 13 3bitr4ri ⊢ ⋃ A = ∅ ↔ A ⊆ ∅