This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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