Metamath Proof Explorer

Theorem uni0c

Description: The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006)

Ref Expression
Assertion uni0c 
|- ( U. A = (/) <-> A. x e. A x = (/) )

Proof

Step Hyp Ref Expression
1 uni0b 
 |-  ( U. A = (/) <-> A C_ { (/) } )
2 dfss3 
 |-  ( A C_ { (/) } <-> A. x e. A x e. { (/) } )
3 velsn 
 |-  ( x e. { (/) } <-> x = (/) )
4 3 ralbii 
 |-  ( A. x e. A x e. { (/) } <-> A. x e. A x = (/) )
5 1 2 4 3bitri 
 |-  ( U. A = (/) <-> A. x e. A x = (/) )