MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uni0b Unicode version

Theorem uni0b 3889
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.)
Assertion
Ref Expression
uni0b  |-  ( U. A  =  (/)  <->  A  C_  { (/) } )

Proof of Theorem uni0b
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elsn 3689 . . 3  |-  ( x  e.  { (/) }  <->  x  =  (/) )
21ralbii 2601 . 2  |-  ( A. x  e.  A  x  e.  { (/) }  <->  A. x  e.  A  x  =  (/) )
3 dfss3 3204 . 2  |-  ( A 
C_  { (/) }  <->  A. x  e.  A  x  e.  {
(/) } )
4 neq0 3499 . . . 4  |-  ( -. 
U. A  =  (/)  <->  E. y  y  e.  U. A
)
5 rexcom4 2841 . . . . 5  |-  ( E. x  e.  A  E. y  y  e.  x  <->  E. y E. x  e.  A  y  e.  x
)
6 neq0 3499 . . . . . 6  |-  ( -.  x  =  (/)  <->  E. y 
y  e.  x )
76rexbii 2602 . . . . 5  |-  ( E. x  e.  A  -.  x  =  (/)  <->  E. x  e.  A  E. y 
y  e.  x )
8 eluni2 3868 . . . . . 6  |-  ( y  e.  U. A  <->  E. x  e.  A  y  e.  x )
98exbii 1573 . . . . 5  |-  ( E. y  y  e.  U. A 
<->  E. y E. x  e.  A  y  e.  x )
105, 7, 93bitr4ri 269 . . . 4  |-  ( E. y  y  e.  U. A 
<->  E. x  e.  A  -.  x  =  (/) )
11 rexnal 2588 . . . 4  |-  ( E. x  e.  A  -.  x  =  (/)  <->  -.  A. x  e.  A  x  =  (/) )
124, 10, 113bitri 262 . . 3  |-  ( -. 
U. A  =  (/)  <->  -.  A. x  e.  A  x  =  (/) )
1312con4bii 288 . 2  |-  ( U. A  =  (/)  <->  A. x  e.  A  x  =  (/) )
142, 3, 133bitr4ri 269 1  |-  ( U. A  =  (/)  <->  A  C_  { (/) } )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   E.wex 1532    = wceq 1633    e. wcel 1701   A.wral 2577   E.wrex 2578    C_ wss 3186   (/)c0 3489   {csn 3674   U.cuni 3864
This theorem is referenced by:  uni0c  3890  uni0  3891  fin1a2lem11  8081  zornn0g  8177  0top  16777  filcon  17630  alexsubALTlem2  17794  ordcmp  25272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-v 2824  df-dif 3189  df-in 3193  df-ss 3200  df-nul 3490  df-sn 3680  df-uni 3865
  Copyright terms: Public domain W3C validator