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

Theorem elpwg 4606
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5345. (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 4008 . 2 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
2 df-pw 4605 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
31, 2elab2g 3671 1 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2107  wss 3949  𝒫 cpw 4603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605
This theorem is referenced by:  elpw  4607  elpwd  4609  elpwi  4610  elpwb  4611  pwidg  4623  elpwunsn  4688  elpwdifsn  4793  prsspwg  4827  elpw2g  5345  snelpwg  5443  pwvrel  5727  eldifpw  7755  elpwun  7756  elpmg  8837  fopwdom  9080  elfpw  9354  rankwflemb  9788  r1elwf  9791  r1pw  9840  ackbij1lem3  10217  lcmfval  16558  lcmf0val  16559  acsfn  17603  evls1val  21839  evls1rhm  21841  evls1sca  21842  fiinopn  22403  clsval2  22554  ssntr  22562  neipeltop  22633  nrmsep3  22859  cnrmi  22864  cmpsublem  22903  conncompss  22937  kgeni  23041  ufileu  23423  filufint  23424  elutop  23738  ustuqtop0  23745  metustss  24060  psmetutop  24076  axtgcont1  27719  elpwincl1  31763  elpwdifcl  31764  elpwiuncl  31765  dispcmp  32839  sigaclci  33130  sigainb  33134  elsigagen2  33146  sigapildsys  33160  ldgenpisyslem1  33161  rossros  33178  measvunilem  33210  measdivcstALTV  33223  ddeval1  33232  ddeval0  33233  omsfval  33293  omssubaddlem  33298  omssubadd  33299  elcarsg  33304  limsucncmpi  35330  bj-elpwg  35933  topdifinffinlem  36228  elrels2  37356  ismrcd1  41436  elpwgded  43325  snelpwrVD  43592  elpwgdedVD  43678  sspwimpcf  43681  sspwimpcfVD  43682  sspwimpALT2  43689  pwpwuni  43744  dvnprodlem1  44662  dvnprodlem2  44663  ovolsplit  44704  stoweidlem50  44766  stoweidlem57  44773  pwsal  45031  salexct  45050  fsumlesge0  45093  sge0f1o  45098  psmeasurelem  45186  omessle  45214  caragensplit  45216  caragenelss  45217  omecl  45219  omeunile  45221  caragenuncl  45229  caragendifcl  45230  omeunle  45232  omeiunlempt  45236  carageniuncllem2  45238  carageniuncl  45239  0ome  45245  caragencmpl  45251  ovnval2  45261  ovncvrrp  45280  ovncl  45283  ovncvr2  45327  hspmbl  45345  isvonmbl  45354  smfresal  45504  gsumlsscl  47059  lincfsuppcl  47094  linccl  47095  lincdifsn  47105  lincellss  47107  ellcoellss  47116  lindslinindimp2lem4  47142  lindslinindsimp2lem5  47143  lindslinindsimp2  47144  lincresunit3lem2  47161  opndisj  47535
  Copyright terms: Public domain W3C validator