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 ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( 𝐴 ∪ 𝐵 ) = ∅ )

Proof

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