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

Theorem pwuni 4178
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
StepHypRef Expression
1 elssuni 3829 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 vex 2766 . . . 4  |-  x  e. 
_V
32elpw 3605 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
41, 3sylibr 205 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
54ssriv 3159 1  |-  A  C_  ~P U. A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    C_ wss 3127   ~Pcpw 3599   U.cuni 3801
This theorem is referenced by:  uniexb  4535  fipwuni  7147  uniwf  7459  rankuni  7503  rankc2  7511  rankxplim  7517  fin23lem17  7932  axcclem  8051  grurn  8391  istopon  16626  eltg3i  16662  cmpfi  17098  hmphdis  17450  ptcmpfi  17467  fbssfi  17495  mopnfss  17952  shsspwh  21786  unfinsef  24436
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-pw 3601  df-uni 3802
  Copyright terms: Public domain W3C validator