Theorem elpw 4571

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

Syntax hints:   ↔ wb 209   ∈ wcel 2149  Vcvv 3463   ⊆ wss 3913  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-pw 4569

This theorem is referenced by:  velpw  4572  0elpw  5327  prelpw  5428  sspwb  5431  pwssun  5554  xpsspw  5797  knatar  7356  iunpw  7770  ssenen  9139  fissuni  9314  fipreima  9315  fipwuni  9386  dffi3  9391  marypha1lem  9393  inf3lem6  9602  tz9.12lem3  9761  rankonidlem  9800  r0weon  9996  infpwfien  10046  dfac5lem4  10110  dfac2b  10114  dfac12lem2  10128  enfin2i  10305  isfin1-3  10370  itunitc1  10404  hsmexlem4  10413  hsmexlem5  10414  axdc4lem  10439  pwfseqlem1  10643  eltsk2g  10736  ixxssxr  13384  ioof  13474  fzof  13684  hashbclem  14489  incexclem  15890  ramub1lem1  17086  ramub1lem2  17087  prdsplusg  17511  prdsmulr  17512  prdsvsca  17513  submrc  17684  isacs2  17709  isssc  17877  homaf  18087  catcfuccl  18175  catcxpccl  18263  clatl  18564  isacs4lem  18600  isacs5lem  18601  dprd2dlem1  20113  ablfac1b  20142  cssval  21801  tgdom  23104  distop  23121  fctop  23130  cctop  23132  ppttop  23133  pptbas  23134  epttop  23135  mretopd  23218  resttopon  23287  dishaus  23508  discmp  23524  cmpsublem  23525  cmpsub  23526  conncompid  23557  2ndcsep  23585  cldllycmp  23621  dislly  23623  iskgen3  23675  kgencn2  23683  txuni2  23691  dfac14  23744  prdstopn  23754  txcmplem1  23767  txcmplem2  23768  hmphdis  23922  fbssfi  23963  trfbas2  23969  uffixsn  24051  hauspwpwf1  24113  alexsubALTlem2  24174  ustuqtop0  24366  met1stc  24647  restmetu  24696  icccmplem1  24949  icccmplem2  24950  opnmbllem  25729  sqff1o  27312  0lt1s  27971  oldf  27996  newf  27997  leftf  28014  rightf  28015  elons2  28417  oncutlt  28423  oniso  28430  onaddscl  28436  onmulscl  28437  onsbnd  28440  incistruhgr  29370  upgrbi  29384  umgrbi  29392  upgr1e  29404  umgredg  29429  uspgr1e  29535  uhgrspansubgrlem  29581  eupth2lems  30530  sspval  31016  foresf1o  32791  cmpcref  34185  esumpcvgval  34413  esumcvg  34421  esum2d  34428  pwsiga  34465  difelsiga  34468  sigainb  34471  pwldsys  34492  rossros  34515  measssd  34550  cntnevol  34563  ddemeas  34571  mbfmcnt  34603  br2base  34604  sxbrsigalem0  34606  oms0  34632  probun  34754  coinfliprv  34818  ballotth  34873  cvmcov2  35666  satfvel  35803  elfuns  36304  altxpsspw  36368  elhf2  36566  neibastop1  36759  neibastop2lem  36760  ctbssinf  37940  opnmbllem0  38195  heiborlem1  38350  heiborlem8  38357  pclfinN  40564  mapd1o  42312  elrfi  43317  ismrcd2  43322  istopclsd  43323  mrefg2  43330  isnacs3  43333  dfac11  43681  islssfg2  43690  lnr2i  43735  clsk1independent  44664  isotone2  44667  gneispace  44752  ismnushort  44903  trsspwALT  45418  trsspwALT2  45419  trsspwALT3  45420  pwtrVD  45424  permaxpow  45610  icof  45827  stoweidlem57  46663  intsal  46936  salexct  46940  sge0resplit  47012  sge0reuz  47053  omeiunltfirp  47125  smfpimbor1lem1  47404  sprvalpw  48118  sprsymrelf  48133  sprsymrelf1  48134  prprvalpw  48153  grimuhgr  48541  uspgropssxp  48798  uspgrsprf  48800