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

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

Proof of Theorem elpw
StepHypRef Expression
1 elpw.1 . 2 𝐴 ∈ V
2 elpwg 4500 . 2 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∈ wcel 2111  Vcvv 3441   ⊆ wss 3881  𝒫 cpw 4497 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499 This theorem is referenced by:  velpw  4502  0elpw  5222  snelpwi  5303  snelpw  5304  prelpw  5305  sspwb  5308  pwssun  5422  xpsspw  5647  knatar  7094  iunpw  7480  ssenen  8682  fissuni  8820  fipreima  8821  fipwuni  8881  dffi3  8886  marypha1lem  8888  inf3lem6  9087  tz9.12lem3  9209  rankonidlem  9248  r0weon  9430  infpwfien  9480  dfac5lem4  9544  dfac2b  9548  dfac12lem2  9562  enfin2i  9739  isfin1-3  9804  itunitc1  9838  hsmexlem4  9847  hsmexlem5  9848  axdc4lem  9873  pwfseqlem1  10076  eltsk2g  10169  ixxssxr  12745  ioof  12832  fzof  13037  hashbclem  13813  incexclem  15190  ramub1lem1  16359  ramub1lem2  16360  prdsplusg  16730  prdsmulr  16731  prdsvsca  16732  submrc  16898  isacs2  16923  isssc  17089  homaf  17289  catcfuccl  17368  catcxpccl  17456  clatl  17725  isacs4lem  17777  isacs5lem  17778  dprd2dlem1  19164  ablfac1b  19193  cssval  20380  tgdom  21597  distop  21614  fctop  21623  cctop  21625  ppttop  21626  pptbas  21627  epttop  21628  mretopd  21711  resttopon  21780  dishaus  22001  discmp  22017  cmpsublem  22018  cmpsub  22019  conncompid  22050  2ndcsep  22078  cldllycmp  22114  dislly  22116  iskgen3  22168  kgencn2  22176  txuni2  22184  dfac14  22237  prdstopn  22247  txcmplem1  22260  txcmplem2  22261  hmphdis  22415  fbssfi  22456  trfbas2  22462  uffixsn  22544  hauspwpwf1  22606  alexsubALTlem2  22667  ustuqtop0  22860  met1stc  23142  restmetu  23191  icccmplem1  23441  icccmplem2  23442  opnmbllem  24219  sqff1o  25781  incistruhgr  26886  upgrbi  26900  umgrbi  26908  upgr1e  26920  umgredg  26945  uspgr1e  27048  uhgrspansubgrlem  27094  eupth2lems  28037  sspval  28520  foresf1o  30287  cmpcref  31239  esumpcvgval  31483  esumcvg  31491  esum2d  31498  pwsiga  31535  difelsiga  31538  sigainb  31541  pwldsys  31562  rossros  31585  measssd  31620  cntnevol  31633  ddemeas  31641  mbfmcnt  31672  br2base  31673  sxbrsigalem0  31675  oms0  31701  probun  31823  coinfliprv  31886  ballotth  31941  cvmcov2  32671  satfvel  32808  elfuns  33525  altxpsspw  33587  elhf2  33785  neibastop1  33856  neibastop2lem  33857  ctbssinf  34863  opnmbllem0  35133  heiborlem1  35289  heiborlem8  35296  pclfinN  37236  mapd1o  38984  elrfi  39699  ismrcd2  39704  istopclsd  39705  mrefg2  39712  isnacs3  39715  dfac11  40070  islssfg2  40079  lnr2i  40124  clsk1independent  40813  isotone2  40816  gneispace  40901  trsspwALT  41588  trsspwALT2  41589  trsspwALT3  41590  pwtrVD  41594  icof  41911  stoweidlem57  42760  intsal  43031  salexct  43035  sge0resplit  43106  sge0reuz  43147  omeiunltfirp  43219  smfpimbor1lem1  43491  sprvalpw  44058  sprsymrelf  44073  sprsymrelf1  44074  prprvalpw  44093  uspgropssxp  44433  uspgrsprf  44435
 Copyright terms: Public domain W3C validator