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

Theorem pwuni 4511
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 4109 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 selpw 3855 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
31, 2sylibr 212 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
43ssriv 3348 1  |-  A  C_  ~P U. A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755    C_ wss 3316   ~Pcpw 3848   U.cuni 4079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850  df-uni 4080
This theorem is referenced by:  uniexb  6375  fipwuni  7664  uniwf  8014  rankuni  8058  rankc2  8066  rankxplim  8074  fin23lem17  8495  axcclem  8614  grurn  8955  istopon  18371  eltg3i  18407  cmpfi  18852  hmphdis  19210  ptcmpfi  19227  fbssfi  19251  mopnfss  19859  shsspwh  24471  hasheuni  26387  issgon  26419  sigaclci  26428  sigagenval  26436  dmsigagen  26440  imambfm  26530
  Copyright terms: Public domain W3C validator