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

Theorem elpwg 4359
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5019. (Contributed by NM, 6-Aug-2000.)
Assertion
Ref Expression
elpwg (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))

Proof of Theorem elpwg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eleq1 2873 . 2 (𝑥 = 𝐴 → (𝑥 ∈ 𝒫 𝐵𝐴 ∈ 𝒫 𝐵))
2 sseq1 3823 . 2 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
3 selpw 4358 . 2 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
41, 2, 3vtoclbg 3460 1 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wcel 2156  wss 3769  𝒫 cpw 4351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-ss 3783  df-pw 4353
This theorem is referenced by:  elpwd  4360  elpwi  4361  elpwb  4362  pwidg  4366  elpwunsn  4417  elpwdifsn  4511  prsspwg  4544  sselpwd  5002  elpw2g  5019  pwel  5110  f1opw2  7118  eldifpw  7206  elpwun  7207  elpmg  8108  fopwdom  8307  elfpw  8507  f1opwfi  8509  rankwflemb  8903  r1elwf  8906  r1pw  8955  ackbij1lem3  9329  ackbij1lem6  9332  ackbij1lem11  9337  lcmfval  15553  lcmf0val  15554  acsfn  16524  evls1val  19893  evls1rhm  19895  evls1sca  19896  fiinopn  20919  clsval2  21068  ssntr  21076  neipeltop  21147  nrmsep3  21373  cnrmi  21378  cmpcov  21406  cmpsublem  21416  conncompss  21450  kgeni  21554  tgqtop  21729  filss  21870  ufileu  21936  filufint  21937  elutop  22250  ustuqtop0  22257  metustss  22569  psmetutop  22585  axtgcont1  25581  elpwincl1  29682  elpwdifcl  29683  elpwiuncl  29684  elpwunicl  29696  dispcmp  30251  pcmplfin  30252  indval  30400  isrnsigaOLD  30500  sigaclci  30520  sigainb  30524  elsigagen2  30536  sigapildsys  30550  ldgenpisyslem1  30551  rossros  30568  measvunilem  30600  measdivcstOLD  30612  ddeval1  30622  ddeval0  30623  omsfval  30681  omssubaddlem  30686  omssubadd  30687  elcarsg  30692  limsucncmpi  32761  topdifinffinlem  33511  elrels2  34549  ismrcd1  37763  elpwgded  39278  snelpwrVD  39560  elpwgdedVD  39647  sspwimpcf  39650  sspwimpcfVD  39651  sspwimpALT2  39658  pwpwuni  39718  wessf1ornlem  39860  dvnprodlem1  40641  dvnprodlem2  40642  ovolsplit  40684  stoweidlem50  40746  stoweidlem57  40753  pwsal  41014  saliuncl  41021  salexct  41031  fsumlesge0  41073  sge0f1o  41078  meadjuni  41153  psmeasurelem  41166  omessle  41194  caragensplit  41196  caragenelss  41197  omecl  41199  omeunile  41201  caragenuncl  41209  caragendifcl  41210  omeunle  41212  omeiunlempt  41216  carageniuncllem2  41218  carageniuncl  41219  0ome  41225  caragencmpl  41231  ovnval2  41241  ovncvrrp  41260  ovncl  41263  ovncvr2  41307  hspmbl  41325  isvonmbl  41334  smfresal  41477  gsumlsscl  42732  lincfsuppcl  42770  linccl  42771  lincdifsn  42781  lincellss  42783  ellcoellss  42792  lindslinindsimp1  42814  lindslinindimp2lem4  42818  lindslinindsimp2lem5  42819  lindslinindsimp2  42820  lincresunit3lem2  42837  lincresunit3  42838
  Copyright terms: Public domain W3C validator