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

Metamath Proof Explorer

Theorem un00

Description: Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004)

Ref Expression
Assertion un00 ⊢ A = ∅ ∧ B = ∅ ↔ A ∪ B = ∅

Proof

Step Hyp Ref Expression
1 uneq12 ⊢ A = ∅ ∧ B = ∅ → A ∪ B = ∅ ∪ ∅
2 un0 ⊢ ∅ ∪ ∅ = ∅
3 1 2 eqtrdi ⊢ A = ∅ ∧ B = ∅ → A ∪ B = ∅
4 ssun1 ⊢ A ⊆ A ∪ B
5 sseq2 ⊢ A ∪ B = ∅ → A ⊆ A ∪ B ↔ A ⊆ ∅
6 4 5 mpbii ⊢ A ∪ B = ∅ → A ⊆ ∅
7 ss0b ⊢ A ⊆ ∅ ↔ A = ∅
8 6 7 sylib ⊢ A ∪ B = ∅ → A = ∅
9 ssun2 ⊢ B ⊆ A ∪ B
10 sseq2 ⊢ A ∪ B = ∅ → B ⊆ A ∪ B ↔ B ⊆ ∅
11 9 10 mpbii ⊢ A ∪ B = ∅ → B ⊆ ∅
12 ss0b ⊢ B ⊆ ∅ ↔ B = ∅
13 11 12 sylib ⊢ A ∪ B = ∅ → B = ∅
14 8 13 jca ⊢ A ∪ B = ∅ → A = ∅ ∧ B = ∅
15 3 14 impbii ⊢ A = ∅ ∧ B = ∅ ↔ A ∪ B = ∅