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

Theorem pwuni 4825
 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 4403 . . 3 (𝑥𝐴𝑥 𝐴)
2 selpw 4115 . . 3 (𝑥 ∈ 𝒫 𝐴𝑥 𝐴)
31, 2sylibr 223 . 2 (𝑥𝐴𝑥 ∈ 𝒫 𝐴)
43ssriv 3572 1 𝐴 ⊆ 𝒫 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108  ∪ cuni 4372 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373 This theorem is referenced by:  uniexb  6866  fipwuni  8215  uniwf  8565  rankuni  8609  rankc2  8617  rankxplim  8625  fin23lem17  9043  axcclem  9162  grurn  9502  istopon  20540  eltg3i  20576  cmpfi  21021  hmphdis  21409  ptcmpfi  21426  fbssfi  21451  mopnfss  22058  shsspwh  27487  circtopn  29232  hasheuni  29474  issgon  29513  sigaclci  29522  sigagenval  29530  dmsigagen  29534  imambfm  29651  salgenval  39217  salgenn0  39225  caragensspw  39399
 Copyright terms: Public domain W3C validator