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

Theorem pwuni 4144
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 3796 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 vex 2743 . . . 4  |-  x  e. 
_V
32elpw 3572 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
41, 3sylibr 205 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
54ssriv 3126 1  |-  A  C_  ~P U. A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    C_ wss 3094   ~Pcpw 3566   U.cuni 3768
This theorem is referenced by:  uniexb  4500  fipwuni  7112  uniwf  7424  rankuni  7468  rankc2  7476  rankxplim  7482  fin23lem17  7897  axcclem  8016  grurn  8356  istopon  16590  eltg3i  16626  cmpfi  17062  hmphdis  17414  ptcmpfi  17431  fbssfi  17459  mopnfss  17916  shsspwh  21750  unfinsef  24400
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-pw 3568  df-uni 3769
  Copyright terms: Public domain W3C validator