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

Theorem elpw 4544
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 4543 . 2 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105  Vcvv 3495  wss 3935  𝒫 cpw 4537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951  df-pw 4539
This theorem is referenced by:  velpw  4545  0elpw  5248  snelpwi  5328  snelpw  5329  prelpw  5330  sspwb  5333  pwssun  5449  xpsspw  5676  knatar  7099  iunpw  7481  ssenen  8680  fissuni  8818  fipreima  8819  fipwuni  8879  dffi3  8884  marypha1lem  8886  inf3lem6  9085  tz9.12lem3  9207  rankonidlem  9246  r0weon  9427  infpwfien  9477  dfac5lem4  9541  dfac2b  9545  dfac12lem2  9559  enfin2i  9732  isfin1-3  9797  itunitc1  9831  hsmexlem4  9840  hsmexlem5  9841  axdc4lem  9866  pwfseqlem1  10069  eltsk2g  10162  ixxssxr  12740  ioof  12825  fzof  13025  hashbclem  13800  incexclem  15181  ramub1lem1  16352  ramub1lem2  16353  prdsplusg  16721  prdsmulr  16722  prdsvsca  16723  submrc  16889  isacs2  16914  isssc  17080  homaf  17280  catcfuccl  17359  catcxpccl  17447  clatl  17716  isacs4lem  17768  isacs5lem  17769  dprd2dlem1  19094  ablfac1b  19123  cssval  20756  tgdom  21516  distop  21533  fctop  21542  cctop  21544  ppttop  21545  pptbas  21546  epttop  21547  mretopd  21630  resttopon  21699  dishaus  21920  discmp  21936  cmpsublem  21937  cmpsub  21938  conncompid  21969  2ndcsep  21997  cldllycmp  22033  dislly  22035  iskgen3  22087  kgencn2  22095  txuni2  22103  dfac14  22156  prdstopn  22166  txcmplem1  22179  txcmplem2  22180  hmphdis  22334  fbssfi  22375  trfbas2  22381  uffixsn  22463  hauspwpwf1  22525  alexsubALTlem2  22586  ustuqtop0  22778  met1stc  23060  restmetu  23109  icccmplem1  23359  icccmplem2  23360  opnmbllem  24131  sqff1o  25687  incistruhgr  26792  upgrbi  26806  umgrbi  26814  upgr1e  26826  umgredg  26851  uspgr1e  26954  uhgrspansubgrlem  27000  eupth2lems  27945  sspval  28428  foresf1o  30193  cmpcref  31014  esumpcvgval  31237  esumcvg  31245  esum2d  31252  pwsiga  31289  difelsiga  31292  sigainb  31295  inelpisys  31313  pwldsys  31316  rossros  31339  measssd  31374  cntnevol  31387  ddemeas  31395  mbfmcnt  31426  br2base  31427  sxbrsigalem0  31429  oms0  31455  probun  31577  coinfliprv  31640  ballotth  31695  cvmcov2  32420  satfvel  32557  elfuns  33274  altxpsspw  33336  elhf2  33534  neibastop1  33605  neibastop2lem  33606  ctbssinf  34570  opnmbllem0  34810  heiborlem1  34972  heiborlem8  34979  pclfinN  36918  mapd1o  38666  elrfi  39171  ismrcd2  39176  istopclsd  39177  mrefg2  39184  isnacs3  39187  dfac11  39542  islssfg2  39551  lnr2i  39596  clsk1independent  40276  isotone2  40279  gneispace  40364  trsspwALT  41032  trsspwALT2  41033  trsspwALT3  41034  pwtrVD  41038  icof  41362  stoweidlem57  42223  intsal  42494  salexct  42498  sge0resplit  42569  sge0reuz  42610  omeiunltfirp  42682  smfpimbor1lem1  42954  sprvalpw  43489  sprsymrelf  43504  sprsymrelf1  43505  prprvalpw  43524  uspgropssxp  43866  uspgrsprf  43868
  Copyright terms: Public domain W3C validator