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

Theorem pwuni 4359
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 4007 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 vex 2923 . . . 4  |-  x  e. 
_V
32elpw 3769 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
41, 3sylibr 204 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
54ssriv 3316 1  |-  A  C_  ~P U. A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721    C_ wss 3284   ~Pcpw 3763   U.cuni 3979
This theorem is referenced by:  uniexb  4715  fipwuni  7393  uniwf  7705  rankuni  7749  rankc2  7757  rankxplim  7763  fin23lem17  8178  axcclem  8297  grurn  8636  istopon  16949  eltg3i  16985  cmpfi  17429  hmphdis  17785  ptcmpfi  17802  fbssfi  17826  mopnfss  18430  shsspwh  22705  hasheuni  24432  issgon  24463  sigaclci  24472  sigagenval  24480  dmsigagen  24484  imambfm  24569
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-in 3291  df-ss 3298  df-pw 3765  df-uni 3980
  Copyright terms: Public domain W3C validator