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

Theorem pwuni 4621
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 4219 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 selpw 3961 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
31, 2sylibr 212 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
43ssriv 3445 1  |-  A  C_  ~P U. A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842    C_ wss 3413   ~Pcpw 3954   U.cuni 4190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-in 3420  df-ss 3427  df-pw 3956  df-uni 4191
This theorem is referenced by:  uniexb  6591  fipwuni  7919  uniwf  8268  rankuni  8312  rankc2  8320  rankxplim  8328  fin23lem17  8749  axcclem  8868  grurn  9208  istopon  19716  eltg3i  19752  cmpfi  20199  hmphdis  20587  ptcmpfi  20604  fbssfi  20628  mopnfss  21236  shsspwh  26564  circtopn  28279  hasheuni  28518  issgon  28557  sigaclci  28566  sigagenval  28574  dmsigagen  28578  imambfm  28696
  Copyright terms: Public domain W3C validator