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