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 u. B ) = (/) )

Proof

Step Hyp Ref Expression
1 uneq12 
 |-  ( ( A = (/) /\ B = (/) ) -> ( A u. B ) = ( (/) u. (/) ) )
2 un0 
 |-  ( (/) u. (/) ) = (/)
3 1 2 eqtrdi 
 |-  ( ( A = (/) /\ B = (/) ) -> ( A u. B ) = (/) )
4 ssun1 
 |-  A C_ ( A u. B )
5 sseq2 
 |-  ( ( A u. B ) = (/) -> ( A C_ ( A u. B ) <-> A C_ (/) ) )
6 4 5 mpbii 
 |-  ( ( A u. B ) = (/) -> A C_ (/) )
7 ss0b 
 |-  ( A C_ (/) <-> A = (/) )
8 6 7 sylib 
 |-  ( ( A u. B ) = (/) -> A = (/) )
9 ssun2 
 |-  B C_ ( A u. B )
10 sseq2 
 |-  ( ( A u. B ) = (/) -> ( B C_ ( A u. B ) <-> B C_ (/) ) )
11 9 10 mpbii 
 |-  ( ( A u. B ) = (/) -> B C_ (/) )
12 ss0b 
 |-  ( B C_ (/) <-> B = (/) )
13 11 12 sylib 
 |-  ( ( A u. B ) = (/) -> B = (/) )
14 8 13 jca 
 |-  ( ( A u. B ) = (/) -> ( A = (/) /\ B = (/) ) )
15 3 14 impbii 
 |-  ( ( A = (/) /\ B = (/) ) <-> ( A u. B ) = (/) )