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