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

Theorem pwuni 4308
Description: A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
Assertion
Ref Expression
pwuni  |-  A  C_  ~P U. A

Proof of Theorem pwuni
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elssuni 3957 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 vex 2876 . . . 4  |-  x  e. 
_V
32elpw 3720 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
41, 3sylibr 203 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
54ssriv 3270 1  |-  A  C_  ~P U. A
Colors of variables: wff set class
Syntax hints:    e. wcel 1715    C_ wss 3238   ~Pcpw 3714   U.cuni 3929
This theorem is referenced by:  uniexb  4666  fipwuni  7326  uniwf  7638  rankuni  7682  rankc2  7690  rankxplim  7696  fin23lem17  8111  axcclem  8230  grurn  8570  istopon  16880  eltg3i  16916  cmpfi  17352  hmphdis  17704  ptcmpfi  17721  fbssfi  17745  mopnfss  18202  shsspwh  22138  hasheuni  23940  issgon  23971  sigaclci  23980  sigagenval  23988  dmsigagen  23992  imambfm  24075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-ss 3252  df-pw 3716  df-uni 3930
  Copyright terms: Public domain W3C validator