Theorem elpw 4553

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-pw 4551

This theorem is referenced by:  velpw  4554  0elpw  5296  prelpw  5389  sspwb  5392  pwssun  5511  xpsspw  5753  knatar  7297  iunpw  7710  ssenen  9071  fissuni  9248  fipreima  9249  fipwuni  9317  dffi3  9322  marypha1lem  9324  inf3lem6  9530  tz9.12lem3  9689  rankonidlem  9728  r0weon  9910  infpwfien  9960  dfac5lem4  10024  dfac5lem4OLD  10026  dfac2b  10029  dfac12lem2  10043  enfin2i  10219  isfin1-3  10284  itunitc1  10318  hsmexlem4  10327  hsmexlem5  10328  axdc4lem  10353  pwfseqlem1  10556  eltsk2g  10649  ixxssxr  13259  ioof  13349  fzof  13558  hashbclem  14361  incexclem  15745  ramub1lem1  16940  ramub1lem2  16941  prdsplusg  17364  prdsmulr  17365  prdsvsca  17366  submrc  17536  isacs2  17561  isssc  17729  homaf  17939  catcfuccl  18027  catcxpccl  18115  clatl  18416  isacs4lem  18452  isacs5lem  18453  dprd2dlem1  19957  ablfac1b  19986  cssval  21621  tgdom  22894  distop  22911  fctop  22920  cctop  22922  ppttop  22923  pptbas  22924  epttop  22925  mretopd  23008  resttopon  23077  dishaus  23298  discmp  23314  cmpsublem  23315  cmpsub  23316  conncompid  23347  2ndcsep  23375  cldllycmp  23411  dislly  23413  iskgen3  23465  kgencn2  23473  txuni2  23481  dfac14  23534  prdstopn  23544  txcmplem1  23557  txcmplem2  23558  hmphdis  23712  fbssfi  23753  trfbas2  23759  uffixsn  23841  hauspwpwf1  23903  alexsubALTlem2  23964  ustuqtop0  24156  met1stc  24437  restmetu  24486  icccmplem1  24739  icccmplem2  24740  opnmbllem  25530  sqff1o  27120  0slt1s  27774  oldf  27799  newf  27800  leftf  27811  rightf  27812  elons2  28196  onscutlt  28202  onsiso  28206  onaddscl  28211  onmulscl  28212  incistruhgr  29059  upgrbi  29073  umgrbi  29081  upgr1e  29093  umgredg  29118  uspgr1e  29224  uhgrspansubgrlem  29270  eupth2lems  30220  sspval  30705  foresf1o  32486  cmpcref  33884  esumpcvgval  34112  esumcvg  34120  esum2d  34127  pwsiga  34164  difelsiga  34167  sigainb  34170  pwldsys  34191  rossros  34214  measssd  34249  cntnevol  34262  ddemeas  34270  mbfmcnt  34302  br2base  34303  sxbrsigalem0  34305  oms0  34331  probun  34453  coinfliprv  34517  ballotth  34572  cvmcov2  35340  satfvel  35477  elfuns  35978  altxpsspw  36042  elhf2  36240  neibastop1  36424  neibastop2lem  36425  ctbssinf  37471  opnmbllem0  37716  heiborlem1  37871  heiborlem8  37878  pclfinN  40019  mapd1o  41767  elrfi  42811  ismrcd2  42816  istopclsd  42817  mrefg2  42824  isnacs3  42827  dfac11  43179  islssfg2  43188  lnr2i  43233  clsk1independent  44163  isotone2  44166  gneispace  44251  ismnushort  44418  trsspwALT  44934  trsspwALT2  44935  trsspwALT3  44936  pwtrVD  44940  permaxpow  45126  icof  45340  stoweidlem57  46179  intsal  46452  salexct  46456  sge0resplit  46528  sge0reuz  46569  omeiunltfirp  46641  smfpimbor1lem1  46920  sprvalpw  47604  sprsymrelf  47619  sprsymrelf1  47620  prprvalpw  47639  grimuhgr  48011  uspgropssxp  48268  uspgrsprf  48270