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

Theorem pwuni 4841
 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 4834 . . 3 (𝑥𝐴𝑥 𝐴)
2 velpw 4505 . . 3 (𝑥 ∈ 𝒫 𝐴𝑥 𝐴)
31, 2sylibr 237 . 2 (𝑥𝐴𝑥 ∈ 𝒫 𝐴)
43ssriv 3921 1 𝐴 ⊆ 𝒫 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2111   ⊆ wss 3883  𝒫 cpw 4500  ∪ cuni 4804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-in 3890  df-ss 3900  df-pw 4502  df-uni 4805 This theorem is referenced by:  uniexr  7478  fipwuni  8892  uniwf  9250  rankuni  9294  rankc2  9302  rankxplim  9310  fin23lem17  9767  axcclem  9886  grurn  10230  istopon  21558  eltg3i  21607  cmpfi  22054  hmphdis  22442  ptcmpfi  22459  fbssfi  22483  mopnfss  23091  pliguhgr  28313  shsspwh  29073  circtopn  31256  hasheuni  31520  issgon  31558  sigaclci  31567  sigagenval  31575  dmsigagen  31579  imambfm  31696  bj-unirel  34619  salgenval  43131  salgenn0  43139  caragensspw  43316
 Copyright terms: Public domain W3C validator