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

Theorem elpwg 4561
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5299. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.)
Assertion
Ref Expression
elpwg (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))

Proof of Theorem elpwg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sseq1 3967 . 2 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
2 df-pw 4560 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
31, 2elab2g 3630 1 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2106  wss 3908  𝒫 cpw 4558
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-in 3915  df-ss 3925  df-pw 4560
This theorem is referenced by:  elpw  4562  elpwd  4564  elpwi  4565  elpwb  4566  pwidg  4578  elpwunsn  4642  elpwdifsn  4747  prsspwg  4781  elpw2g  5299  snelpwg  5397  pwvrel  5680  eldifpw  7698  elpwun  7699  elpmg  8777  fopwdom  9020  elfpw  9294  rankwflemb  9725  r1elwf  9728  r1pw  9777  ackbij1lem3  10154  lcmfval  16489  lcmf0val  16490  acsfn  17531  evls1val  21670  evls1rhm  21672  evls1sca  21673  fiinopn  22234  clsval2  22385  ssntr  22393  neipeltop  22464  nrmsep3  22690  cnrmi  22695  cmpsublem  22734  conncompss  22768  kgeni  22872  ufileu  23254  filufint  23255  elutop  23569  ustuqtop0  23576  metustss  23891  psmetutop  23907  axtgcont1  27296  elpwincl1  31339  elpwdifcl  31340  elpwiuncl  31341  dispcmp  32309  sigaclci  32600  sigainb  32604  elsigagen2  32616  sigapildsys  32630  ldgenpisyslem1  32631  rossros  32648  measvunilem  32680  measdivcstALTV  32693  ddeval1  32702  ddeval0  32703  omsfval  32763  omssubaddlem  32768  omssubadd  32769  elcarsg  32774  limsucncmpi  34884  bj-elpwg  35490  topdifinffinlem  35785  elrels2  36915  ismrcd1  40959  elpwgded  42788  snelpwrVD  43055  elpwgdedVD  43141  sspwimpcf  43144  sspwimpcfVD  43145  sspwimpALT2  43152  pwpwuni  43207  dvnprodlem1  44119  dvnprodlem2  44120  ovolsplit  44161  stoweidlem50  44223  stoweidlem57  44230  pwsal  44488  salexct  44507  fsumlesge0  44550  sge0f1o  44555  psmeasurelem  44643  omessle  44671  caragensplit  44673  caragenelss  44674  omecl  44676  omeunile  44678  caragenuncl  44686  caragendifcl  44687  omeunle  44689  omeiunlempt  44693  carageniuncllem2  44695  carageniuncl  44696  0ome  44702  caragencmpl  44708  ovnval2  44718  ovncvrrp  44737  ovncl  44740  ovncvr2  44784  hspmbl  44802  isvonmbl  44811  smfresal  44961  gsumlsscl  46391  lincfsuppcl  46426  linccl  46427  lincdifsn  46437  lincellss  46439  ellcoellss  46448  lindslinindimp2lem4  46474  lindslinindsimp2lem5  46475  lindslinindsimp2  46476  lincresunit3lem2  46493  opndisj  46867
  Copyright terms: Public domain W3C validator