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 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  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  7694  elpwun  7695  elpmg  8739  fopwdom  8982  elfpw  9256  rankwflemb  9687  r1elwf  9690  r1pw  9739  ackbij1lem3  10116  lcmfval  16457  lcmf0val  16458  acsfn  17499  evls1val  21638  evls1rhm  21640  evls1sca  21641  fiinopn  22202  clsval2  22353  ssntr  22361  neipeltop  22432  nrmsep3  22658  cnrmi  22663  cmpsublem  22702  conncompss  22736  kgeni  22840  ufileu  23222  filufint  23223  elutop  23537  ustuqtop0  23544  metustss  23859  psmetutop  23875  axtgcont1  27239  elpwincl1  31282  elpwdifcl  31283  elpwiuncl  31284  dispcmp  32252  sigaclci  32543  sigainb  32547  elsigagen2  32559  sigapildsys  32573  ldgenpisyslem1  32574  rossros  32591  measvunilem  32623  measdivcstALTV  32636  ddeval1  32645  ddeval0  32646  omsfval  32706  omssubaddlem  32711  omssubadd  32712  elcarsg  32717  limsucncmpi  34855  bj-elpwg  35461  topdifinffinlem  35756  elrels2  36886  ismrcd1  40930  elpwgded  42757  snelpwrVD  43024  elpwgdedVD  43110  sspwimpcf  43113  sspwimpcfVD  43114  sspwimpALT2  43121  pwpwuni  43176  dvnprodlem1  44088  dvnprodlem2  44089  ovolsplit  44130  stoweidlem50  44192  stoweidlem57  44199  pwsal  44457  salexct  44476  fsumlesge0  44519  sge0f1o  44524  psmeasurelem  44612  omessle  44640  caragensplit  44642  caragenelss  44643  omecl  44645  omeunile  44647  caragenuncl  44655  caragendifcl  44656  omeunle  44658  omeiunlempt  44662  carageniuncllem2  44664  carageniuncl  44665  0ome  44671  caragencmpl  44677  ovnval2  44687  ovncvrrp  44706  ovncl  44709  ovncvr2  44753  hspmbl  44771  isvonmbl  44780  smfresal  44930  gsumlsscl  46360  lincfsuppcl  46395  linccl  46396  lincdifsn  46406  lincellss  46408  ellcoellss  46417  lindslinindimp2lem4  46443  lindslinindsimp2lem5  46444  lindslinindsimp2  46445  lincresunit3lem2  46462  opndisj  46836
  Copyright terms: Public domain W3C validator