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

Theorem elpw 4320
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
elpw.1 𝐴 ∈ V
Assertion
Ref Expression
elpw (𝐴 ∈ 𝒫 𝐵𝐴𝐵)

Proof of Theorem elpw
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elpw.1 . 2 𝐴 ∈ V
2 sseq1 3785 . 2 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
3 df-pw 4316 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
41, 2, 3elab2 3508 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wcel 2155  Vcvv 3349  wss 3731  𝒫 cpw 4314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-v 3351  df-in 3738  df-ss 3745  df-pw 4316
This theorem is referenced by:  selpw  4321  0elpw  4991  snelpwi  5067  snelpw  5068  prelpw  5069  sspwb  5072  pwssun  5180  xpsspw  5400  knatar  6798  iunpw  7175  ssenen  8340  fissuni  8477  fipreima  8478  fiin  8534  fipwuni  8538  dffi3  8543  marypha1lem  8545  inf3lem6  8744  tz9.12lem3  8866  rankonidlem  8905  r0weon  9085  infpwfien  9135  dfac5lem4  9199  dfac2b  9203  dfac2OLD  9205  dfac12lem2  9218  enfin2i  9395  isfin1-3  9460  itunitc1  9494  hsmexlem4  9503  hsmexlem5  9504  axdc4lem  9529  pwfseqlem1  9732  eltsk2g  9825  ixxssxr  12388  ioof  12473  fzof  12674  hashbclem  13436  incexclem  14853  ramub1lem1  16010  ramub1lem2  16011  prdsplusg  16385  prdsmulr  16386  prdsvsca  16387  submrc  16555  isacs2  16580  isssc  16746  homaf  16946  catcfuccl  17025  catcxpccl  17114  clatl  17383  fpwipodrs  17431  isacs4lem  17435  isacs5lem  17436  dprd2dlem1  18706  ablfac1b  18735  cssval  20301  tgdom  21061  distop  21078  fctop  21087  cctop  21089  ppttop  21090  pptbas  21091  epttop  21092  mretopd  21175  resttopon  21244  dishaus  21465  discmp  21480  cmpsublem  21481  cmpsub  21482  conncompid  21513  2ndcsep  21541  cldllycmp  21577  dislly  21579  iskgen3  21631  kgencn2  21639  txuni2  21647  dfac14  21700  prdstopn  21710  txcmplem1  21723  txcmplem2  21724  hmphdis  21878  fbssfi  21919  trfbas2  21925  uffixsn  22007  hauspwpwf1  22069  alexsubALTlem2  22130  ustuqtop0  22322  met1stc  22604  restmetu  22653  icccmplem1  22903  icccmplem2  22904  opnmbllem  23658  sqff1o  25198  incistruhgr  26250  upgrbi  26264  umgrbi  26272  upgr1e  26284  umgredg  26310  uspgr1e  26414  uhgrspansubgrlem  26460  eupth2lems  27473  sspval  27968  foresf1o  29726  cmpcref  30298  esumpcvgval  30521  esumcvg  30529  esum2d  30536  pwsiga  30574  difelsiga  30577  sigainb  30580  inelpisys  30598  pwldsys  30601  rossros  30624  measssd  30659  cntnevol  30672  ddemeas  30680  mbfmcnt  30711  br2base  30712  sxbrsigalem0  30714  oms0  30740  probun  30863  coinfliprv  30926  ballotth  30981  cvmcov2  31636  dmscut  32293  elfuns  32397  altxpsspw  32459  elhf2  32657  neibastop1  32728  neibastop2lem  32729  opnmbllem0  33801  heiborlem1  33964  heiborlem8  33971  pclfinN  35788  mapd1o  37536  elrfi  37867  ismrcd2  37872  istopclsd  37873  mrefg2  37880  isnacs3  37883  dfac11  38241  islssfg2  38250  lnr2i  38295  clsk1independent  38950  isotone1  38952  isotone2  38953  gneispace  39038  trsspwALT  39638  trsspwALT2  39639  trsspwALT3  39640  pwtrVD  39644  icof  39988  stoweidlem57  40843  intsal  41117  salexct  41121  sge0resplit  41192  sge0reuz  41233  omeiunltfirp  41305  smfpimbor1lem1  41577  sprvalpw  42331  sprsymrelf  42346  sprsymrelf1  42347  uspgropssxp  42353  uspgrsprf  42355
  Copyright terms: Public domain W3C validator