Theorem uni0b

Description: The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004)

	Ref	Expression
Assertion	uni0b	|- ( U. A = (/) <-> A C_ { (/) } )

Proof

Step	Hyp	Ref	Expression
1		velsn	|- ( x e. { (/) } <-> x = (/) )
2	1	ralbii	|- ( A. x e. A x e. { (/) } <-> A. x e. A x = (/) )
3		dfss3	|- ( A C_ { (/) } <-> A. x e. A x e. { (/) } )
4		neq0	|- ( -. U. A = (/) <-> E. y y e. U. A )
5		rexcom4	|- ( E. x e. A E. y y e. x <-> E. y E. x e. A y e. x )
6		neq0	|- ( -. x = (/) <-> E. y y e. x )
7	6	rexbii	|- ( E. x e. A -. x = (/) <-> E. x e. A E. y y e. x )
8		eluni2	|- ( y e. U. A <-> E. x e. A y e. x )
9	8	exbii	|- ( E. y y e. U. A <-> E. y E. x e. A y e. x )
10	5 7 9	3bitr4ri	|- ( E. y y e. U. A <-> E. x e. A -. x = (/) )
11		rexnal	|- ( E. x e. A -. x = (/) <-> -. A. x e. A x = (/) )
12	4 10 11	3bitri	|- ( -. U. A = (/) <-> -. A. x e. A x = (/) )
13	12	con4bii	|- ( U. A = (/) <-> A. x e. A x = (/) )
14	2 3 13	3bitr4ri	|- ( U. A = (/) <-> A C_ { (/) } )