Theorem elpw 4567

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 4566	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  𝒫 cpw 4563

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-pw 4565

This theorem is referenced by:  velpw  4568  0elpw  5311  snelpwiOLD  5404  prelpw  5406  sspwb  5409  pwssun  5530  xpsspw  5772  knatar  7332  iunpw  7747  ssenen  9115  fissuni  9308  fipreima  9309  fipwuni  9377  dffi3  9382  marypha1lem  9384  inf3lem6  9586  tz9.12lem3  9742  rankonidlem  9781  r0weon  9965  infpwfien  10015  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  dfac12lem2  10098  enfin2i  10274  isfin1-3  10339  itunitc1  10373  hsmexlem4  10382  hsmexlem5  10383  axdc4lem  10408  pwfseqlem1  10611  eltsk2g  10704  ixxssxr  13318  ioof  13408  fzof  13617  hashbclem  14417  incexclem  15802  ramub1lem1  16997  ramub1lem2  16998  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  submrc  17589  isacs2  17614  isssc  17782  homaf  17992  catcfuccl  18080  catcxpccl  18168  clatl  18467  isacs4lem  18503  isacs5lem  18504  dprd2dlem1  19973  ablfac1b  20002  cssval  21591  tgdom  22865  distop  22882  fctop  22891  cctop  22893  ppttop  22894  pptbas  22895  epttop  22896  mretopd  22979  resttopon  23048  dishaus  23269  discmp  23285  cmpsublem  23286  cmpsub  23287  conncompid  23318  2ndcsep  23346  cldllycmp  23382  dislly  23384  iskgen3  23436  kgencn2  23444  txuni2  23452  dfac14  23505  prdstopn  23515  txcmplem1  23528  txcmplem2  23529  hmphdis  23683  fbssfi  23724  trfbas2  23730  uffixsn  23812  hauspwpwf1  23874  alexsubALTlem2  23935  ustuqtop0  24128  met1stc  24409  restmetu  24458  icccmplem1  24711  icccmplem2  24712  opnmbllem  25502  sqff1o  27092  0slt1s  27741  oldf  27765  newf  27766  leftf  27777  rightf  27778  elons2  28159  onscutlt  28165  onsiso  28169  onaddscl  28174  onmulscl  28175  incistruhgr  29006  upgrbi  29020  umgrbi  29028  upgr1e  29040  umgredg  29065  uspgr1e  29171  uhgrspansubgrlem  29217  eupth2lems  30167  sspval  30652  foresf1o  32433  cmpcref  33840  esumpcvgval  34068  esumcvg  34076  esum2d  34083  pwsiga  34120  difelsiga  34123  sigainb  34126  pwldsys  34147  rossros  34170  measssd  34205  cntnevol  34218  ddemeas  34226  mbfmcnt  34259  br2base  34260  sxbrsigalem0  34262  oms0  34288  probun  34410  coinfliprv  34474  ballotth  34529  cvmcov2  35262  satfvel  35399  elfuns  35903  altxpsspw  35965  elhf2  36163  neibastop1  36347  neibastop2lem  36348  ctbssinf  37394  opnmbllem0  37650  heiborlem1  37805  heiborlem8  37812  pclfinN  39894  mapd1o  41642  elrfi  42682  ismrcd2  42687  istopclsd  42688  mrefg2  42695  isnacs3  42698  dfac11  43051  islssfg2  43060  lnr2i  43105  clsk1independent  44035  isotone2  44038  gneispace  44123  ismnushort  44290  trsspwALT  44807  trsspwALT2  44808  trsspwALT3  44809  pwtrVD  44813  permaxpow  44999  icof  45213  stoweidlem57  46055  intsal  46328  salexct  46332  sge0resplit  46404  sge0reuz  46445  omeiunltfirp  46517  smfpimbor1lem1  46796  sprvalpw  47481  sprsymrelf  47496  sprsymrelf1  47497  prprvalpw  47516  grimuhgr  47887  uspgropssxp  48132  uspgrsprf  48134