Metamath Proof Explorer

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_ { (/) } )