Theorem elpw 4558

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

Syntax hints:   ↔ wb 208   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3904  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-pw 4556

This theorem is referenced by:  velpw  4559  0elpw  5311  prelpw  5412  sspwb  5415  pwssun  5537  xpsspw  5780  knatar  7337  iunpw  7750  ssenen  9119  fissuni  9297  fipreima  9298  fipwuni  9369  dffi3  9374  marypha1lem  9376  inf3lem6  9585  tz9.12lem3  9744  rankonidlem  9783  r0weon  9965  infpwfien  10015  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  dfac12lem2  10098  enfin2i  10275  isfin1-3  10340  itunitc1  10374  hsmexlem4  10383  hsmexlem5  10384  axdc4lem  10409  pwfseqlem1  10613  eltsk2g  10706  ixxssxr  13358  ioof  13448  fzof  13658  hashbclem  14462  incexclem  15849  ramub1lem1  17045  ramub1lem2  17046  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  submrc  17643  isacs2  17668  isssc  17836  homaf  18046  catcfuccl  18134  catcxpccl  18222  clatl  18523  isacs4lem  18559  isacs5lem  18560  dprd2dlem1  20066  ablfac1b  20095  cssval  21714  tgdom  23018  distop  23035  fctop  23044  cctop  23046  ppttop  23047  pptbas  23048  epttop  23049  mretopd  23132  resttopon  23201  dishaus  23422  discmp  23438  cmpsublem  23439  cmpsub  23440  conncompid  23471  2ndcsep  23499  cldllycmp  23535  dislly  23537  iskgen3  23589  kgencn2  23597  txuni2  23605  dfac14  23658  prdstopn  23668  txcmplem1  23681  txcmplem2  23682  hmphdis  23836  fbssfi  23877  trfbas2  23883  uffixsn  23965  hauspwpwf1  24027  alexsubALTlem2  24088  ustuqtop0  24280  met1stc  24561  restmetu  24610  icccmplem1  24863  icccmplem2  24864  opnmbllem  25643  sqff1o  27223  0lt1s  27882  oldf  27907  newf  27908  leftf  27925  rightf  27926  elons2  28328  oncutlt  28334  oniso  28341  onaddscl  28347  onmulscl  28348  onsbnd  28351  incistruhgr  29226  upgrbi  29240  umgrbi  29248  upgr1e  29260  umgredg  29285  uspgr1e  29391  uhgrspansubgrlem  29437  eupth2lems  30386  sspval  30872  foresf1o  32652  cmpcref  34108  esumpcvgval  34336  esumcvg  34344  esum2d  34351  pwsiga  34388  difelsiga  34391  sigainb  34394  pwldsys  34415  rossros  34438  measssd  34473  cntnevol  34486  ddemeas  34494  mbfmcnt  34526  br2base  34527  sxbrsigalem0  34529  oms0  34555  probun  34677  coinfliprv  34741  ballotth  34796  cvmcov2  35589  satfvel  35726  elfuns  36227  altxpsspw  36291  elhf2  36489  neibastop1  36683  neibastop2lem  36684  ctbssinf  37864  opnmbllem0  38119  heiborlem1  38274  heiborlem8  38281  pclfinN  40488  mapd1o  42236  elrfi  43239  ismrcd2  43244  istopclsd  43245  mrefg2  43252  isnacs3  43255  dfac11  43603  islssfg2  43612  lnr2i  43657  clsk1independent  44586  isotone2  44589  gneispace  44674  ismnushort  44841  trsspwALT  45357  trsspwALT2  45358  trsspwALT3  45359  pwtrVD  45363  permaxpow  45549  icof  45759  stoweidlem57  46595  intsal  46868  salexct  46872  sge0resplit  46944  sge0reuz  46985  omeiunltfirp  47057  smfpimbor1lem1  47336  sprvalpw  48050  sprsymrelf  48065  sprsymrelf1  48066  prprvalpw  48085  grimuhgr  48473  uspgropssxp  48730  uspgrsprf  48732