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

Theorem pwuni 4353
 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

Proof of Theorem pwuni
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elssuni 4001 . . 3
2 vex 2917 . . . 4
32elpw 3763 . . 3
41, 3sylibr 204 . 2
54ssriv 3310 1
 Colors of variables: wff set class Syntax hints:   wcel 1721   wss 3278  cpw 3757  cuni 3973 This theorem is referenced by:  uniexb  4709  fipwuni  7387  uniwf  7699  rankuni  7743  rankc2  7751  rankxplim  7757  fin23lem17  8172  axcclem  8291  grurn  8630  istopon  16941  eltg3i  16977  cmpfi  17421  hmphdis  17777  ptcmpfi  17794  fbssfi  17818  mopnfss  18422  shsspwh  22697  hasheuni  24426  issgon  24457  sigaclci  24466  sigagenval  24474  dmsigagen  24478  imambfm  24563 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 2383 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2389  df-cleq 2395  df-clel 2398  df-nfc 2527  df-v 2916  df-in 3285  df-ss 3292  df-pw 3759  df-uni 3974
 Copyright terms: Public domain W3C validator