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

Theorem pwuni 4618
 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 4611 . . 3 (𝑥𝐴𝑥 𝐴)
2 selpw 4301 . . 3 (𝑥 ∈ 𝒫 𝐴𝑥 𝐴)
31, 2sylibr 224 . 2 (𝑥𝐴𝑥 ∈ 𝒫 𝐴)
43ssriv 3740 1 𝐴 ⊆ 𝒫 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2131   ⊆ wss 3707  𝒫 cpw 4294  ∪ cuni 4580 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-in 3714  df-ss 3721  df-pw 4296  df-uni 4581 This theorem is referenced by:  uniexr  7129  fipwuni  8489  uniwf  8847  rankuni  8891  rankc2  8899  rankxplim  8907  fin23lem17  9344  axcclem  9463  grurn  9807  istopon  20911  eltg3i  20959  cmpfi  21405  hmphdis  21793  ptcmpfi  21810  fbssfi  21834  mopnfss  22441  pliguhgr  27641  shsspwh  28404  circtopn  30205  hasheuni  30448  issgon  30487  sigaclci  30496  sigagenval  30504  dmsigagen  30508  imambfm  30625  salgenval  41036  salgenn0  41044  caragensspw  41221
 Copyright terms: Public domain W3C validator