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

Theorem elpwg 4547
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5243. (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 3995 . 2 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
2 df-pw 4543 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
31, 2elab2g 3672 1 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wcel 2107  wss 3939  𝒫 cpw 4541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-in 3946  df-ss 3955  df-pw 4543
This theorem is referenced by:  elpw  4548  elpwd  4552  elpwi  4553  elpwb  4554  pwidg  4558  elpwunsn  4619  elpwdifsn  4719  prsspwg  4754  elpw2g  5243  pwvrel  5600  eldifpw  7482  elpwun  7483  elpmg  8415  fopwdom  8617  elfpw  8818  rankwflemb  9214  r1elwf  9217  r1pw  9266  ackbij1lem3  9636  lcmfval  15957  lcmf0val  15958  acsfn  16922  evls1val  20400  evls1rhm  20402  evls1sca  20403  fiinopn  21425  clsval2  21574  ssntr  21582  neipeltop  21653  nrmsep3  21879  cnrmi  21884  cmpsublem  21923  conncompss  21957  kgeni  22061  ufileu  22443  filufint  22444  elutop  22757  ustuqtop0  22764  metustss  23076  psmetutop  23092  axtgcont1  26168  elpwincl1  30200  elpwdifcl  30201  elpwiuncl  30202  elpwunicl  30221  dispcmp  31009  sigaclci  31277  sigainb  31281  elsigagen2  31293  sigapildsys  31307  ldgenpisyslem1  31308  rossros  31325  measvunilem  31357  measdivcstALTV  31370  ddeval1  31379  ddeval0  31380  omsfval  31438  omssubaddlem  31443  omssubadd  31444  elcarsg  31449  limsucncmpi  33677  bj-elpwg  34226  topdifinffinlem  34497  elrels2  35593  ismrcd1  39156  elpwgded  40759  snelpwrVD  41026  elpwgdedVD  41112  sspwimpcf  41115  sspwimpcfVD  41116  sspwimpALT2  41123  pwpwuni  41180  dvnprodlem1  42092  dvnprodlem2  42093  ovolsplit  42135  stoweidlem50  42197  stoweidlem57  42204  pwsal  42462  saliuncl  42469  salexct  42479  fsumlesge0  42521  sge0f1o  42526  psmeasurelem  42614  omessle  42642  caragensplit  42644  caragenelss  42645  omecl  42647  omeunile  42649  caragenuncl  42657  caragendifcl  42658  omeunle  42660  omeiunlempt  42664  carageniuncllem2  42666  carageniuncl  42667  0ome  42673  caragencmpl  42679  ovnval2  42689  ovncvrrp  42708  ovncl  42711  ovncvr2  42755  hspmbl  42773  isvonmbl  42782  smfresal  42925  gsumlsscl  44259  lincfsuppcl  44296  linccl  44297  lincdifsn  44307  lincellss  44309  ellcoellss  44318  lindslinindimp2lem4  44344  lindslinindsimp2lem5  44345  lindslinindsimp2  44346  lincresunit3lem2  44363
  Copyright terms: Public domain W3C validator