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

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 ( ∪ 𝐴 = ∅ ↔ 𝐴 ⊆ { ∅ } )

Proof

Step Hyp Ref Expression
1 velsn ⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
2 1 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { ∅ } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = ∅ )
3 dfss3 ⊢ ( 𝐴 ⊆ { ∅ } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { ∅ } )
4 neq0 ⊢ ( ¬ ∪ 𝐴 = ∅ ↔ ∃ 𝑦 𝑦 ∈ ∪ 𝐴 )
5 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ 𝑥 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
6 neq0 ⊢ ( ¬ 𝑥 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
7 6 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ 𝑥 )
8 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
9 8 exbii ⊢ ( ∃ 𝑦 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
10 5 7 9 3bitr4ri ⊢ ( ∃ 𝑦 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 = ∅ )
11 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 = ∅ ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 = ∅ )
12 4 10 11 3bitri ⊢ ( ¬ ∪ 𝐴 = ∅ ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 = ∅ )
13 12 con4bii ⊢ ( ∪ 𝐴 = ∅ ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = ∅ )
14 2 3 13 3bitr4ri ⊢ ( ∪ 𝐴 = ∅ ↔ 𝐴 ⊆ { ∅ } )