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

Theorem pwuni 4208
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 3857 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 vex 2793 . . . 4  |-  x  e. 
_V
32elpw 3633 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
41, 3sylibr 203 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
54ssriv 3186 1  |-  A  C_  ~P U. A
Colors of variables: wff set class
Syntax hints:    e. wcel 1686    C_ wss 3154   ~Pcpw 3627   U.cuni 3829
This theorem is referenced by:  uniexb  4565  fipwuni  7181  uniwf  7493  rankuni  7537  rankc2  7545  rankxplim  7551  fin23lem17  7966  axcclem  8085  grurn  8425  istopon  16665  eltg3i  16701  cmpfi  17137  hmphdis  17489  ptcmpfi  17506  fbssfi  17534  mopnfss  17991  shsspwh  21827  hasheuni  23455  issgon  23486  sigaclci  23495  sigagenval  23503  dmsigagen  23507  imambfm  23569  unfinsef  25080
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168  df-pw 3629  df-uni 3830
  Copyright terms: Public domain W3C validator