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

Theorem pwuni 4472
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 4465 . . 3 (𝑥𝐴𝑥 𝐴)
2 selpw 4163 . . 3 (𝑥 ∈ 𝒫 𝐴𝑥 𝐴)
31, 2sylibr 224 . 2 (𝑥𝐴𝑥 ∈ 𝒫 𝐴)
43ssriv 3605 1 𝐴 ⊆ 𝒫 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  wss 3572  𝒫 cpw 4156   cuni 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-ss 3586  df-pw 4158  df-uni 4435
This theorem is referenced by:  uniexr  6969  fipwuni  8329  uniwf  8679  rankuni  8723  rankc2  8731  rankxplim  8739  fin23lem17  9157  axcclem  9276  grurn  9620  istopon  20711  eltg3i  20759  cmpfi  21205  hmphdis  21593  ptcmpfi  21610  fbssfi  21635  mopnfss  22242  pliguhgr  27322  shsspwh  28087  circtopn  29889  hasheuni  30132  issgon  30171  sigaclci  30180  sigagenval  30188  dmsigagen  30192  imambfm  30309  salgenval  40310  salgenn0  40318  caragensspw  40492
  Copyright terms: Public domain W3C validator