Theorem elpw 4570

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

Step	Hyp	Ref	Expression
1		elpw.1	. 2 ⊢ 𝐴 ∈ V
2		elpwg 4569	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917  𝒫 cpw 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-pw 4568

This theorem is referenced by:  velpw  4571  0elpw  5314  snelpwiOLD  5407  prelpw  5409  sspwb  5412  pwssun  5533  xpsspw  5775  knatar  7335  iunpw  7750  ssenen  9121  fissuni  9315  fipreima  9316  fipwuni  9384  dffi3  9389  marypha1lem  9391  inf3lem6  9593  tz9.12lem3  9749  rankonidlem  9788  r0weon  9972  infpwfien  10022  dfac5lem4  10086  dfac5lem4OLD  10088  dfac2b  10091  dfac12lem2  10105  enfin2i  10281  isfin1-3  10346  itunitc1  10380  hsmexlem4  10389  hsmexlem5  10390  axdc4lem  10415  pwfseqlem1  10618  eltsk2g  10711  ixxssxr  13325  ioof  13415  fzof  13624  hashbclem  14424  incexclem  15809  ramub1lem1  17004  ramub1lem2  17005  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  submrc  17596  isacs2  17621  isssc  17789  homaf  17999  catcfuccl  18087  catcxpccl  18175  clatl  18474  isacs4lem  18510  isacs5lem  18511  dprd2dlem1  19980  ablfac1b  20009  cssval  21598  tgdom  22872  distop  22889  fctop  22898  cctop  22900  ppttop  22901  pptbas  22902  epttop  22903  mretopd  22986  resttopon  23055  dishaus  23276  discmp  23292  cmpsublem  23293  cmpsub  23294  conncompid  23325  2ndcsep  23353  cldllycmp  23389  dislly  23391  iskgen3  23443  kgencn2  23451  txuni2  23459  dfac14  23512  prdstopn  23522  txcmplem1  23535  txcmplem2  23536  hmphdis  23690  fbssfi  23731  trfbas2  23737  uffixsn  23819  hauspwpwf1  23881  alexsubALTlem2  23942  ustuqtop0  24135  met1stc  24416  restmetu  24465  icccmplem1  24718  icccmplem2  24719  opnmbllem  25509  sqff1o  27099  0slt1s  27748  oldf  27772  newf  27773  leftf  27784  rightf  27785  elons2  28166  onscutlt  28172  onsiso  28176  onaddscl  28181  onmulscl  28182  incistruhgr  29013  upgrbi  29027  umgrbi  29035  upgr1e  29047  umgredg  29072  uspgr1e  29178  uhgrspansubgrlem  29224  eupth2lems  30174  sspval  30659  foresf1o  32440  cmpcref  33847  esumpcvgval  34075  esumcvg  34083  esum2d  34090  pwsiga  34127  difelsiga  34130  sigainb  34133  pwldsys  34154  rossros  34177  measssd  34212  cntnevol  34225  ddemeas  34233  mbfmcnt  34266  br2base  34267  sxbrsigalem0  34269  oms0  34295  probun  34417  coinfliprv  34481  ballotth  34536  cvmcov2  35269  satfvel  35406  elfuns  35910  altxpsspw  35972  elhf2  36170  neibastop1  36354  neibastop2lem  36355  ctbssinf  37401  opnmbllem0  37657  heiborlem1  37812  heiborlem8  37819  pclfinN  39901  mapd1o  41649  elrfi  42689  ismrcd2  42694  istopclsd  42695  mrefg2  42702  isnacs3  42705  dfac11  43058  islssfg2  43067  lnr2i  43112  clsk1independent  44042  isotone2  44045  gneispace  44130  ismnushort  44297  trsspwALT  44814  trsspwALT2  44815  trsspwALT3  44816  pwtrVD  44820  permaxpow  45006  icof  45220  stoweidlem57  46062  intsal  46335  salexct  46339  sge0resplit  46411  sge0reuz  46452  omeiunltfirp  46524  smfpimbor1lem1  46803  sprvalpw  47485  sprsymrelf  47500  sprsymrelf1  47501  prprvalpw  47520  grimuhgr  47891  uspgropssxp  48136  uspgrsprf  48138