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

Theorem pwuni 4205
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 3856 . . 3  |-  ( x  e.  A  ->  x  C_ 
U. A )
2 vex 2792 . . . 4  |-  x  e. 
_V
32elpw 3632 . . 3  |-  ( x  e.  ~P U. A  <->  x 
C_  U. A )
41, 3sylibr 203 . 2  |-  ( x  e.  A  ->  x  e.  ~P U. A )
54ssriv 3185 1  |-  A  C_  ~P U. A
Colors of variables: wff set class
Syntax hints:    e. wcel 1685    C_ wss 3153   ~Pcpw 3626   U.cuni 3828
This theorem is referenced by:  uniexb  4562  fipwuni  7175  uniwf  7487  rankuni  7531  rankc2  7539  rankxplim  7545  fin23lem17  7960  axcclem  8079  grurn  8419  istopon  16659  eltg3i  16695  cmpfi  17131  hmphdis  17483  ptcmpfi  17500  fbssfi  17528  mopnfss  17985  shsspwh  21821  unfinsef  24479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628  df-uni 3829
  Copyright terms: Public domain W3C validator