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 209   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3906  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3923  df-pw 4565

This theorem is referenced by:  velpw  4568  0elpw  5328  prelpw  5429  sspwb  5432  pwssun  5555  xpsspw  5798  knatar  7357  iunpw  7771  ssenen  9140  fissuni  9315  fipreima  9316  fipwuni  9387  dffi3  9392  marypha1lem  9394  inf3lem6  9603  tz9.12lem3  9762  rankonidlem  9801  r0weon  9997  infpwfien  10047  dfac5lem4  10111  dfac2b  10115  dfac12lem2  10129  enfin2i  10306  isfin1-3  10371  itunitc1  10405  hsmexlem4  10414  hsmexlem5  10415  axdc4lem  10440  pwfseqlem1  10644  eltsk2g  10737  ixxssxr  13385  ioof  13475  fzof  13686  hashbclem  14491  incexclem  15892  ramub1lem1  17087  ramub1lem2  17088  prdsplusg  17512  prdsmulr  17513  prdsvsca  17514  submrc  17685  isacs2  17710  isssc  17878  homaf  18088  catcfuccl  18176  catcxpccl  18264  clatl  18565  isacs4lem  18601  isacs5lem  18602  dprd2dlem1  20114  ablfac1b  20143  cssval  21813  tgdom  23116  distop  23133  fctop  23142  cctop  23144  ppttop  23145  pptbas  23146  epttop  23147  mretopd  23230  resttopon  23299  dishaus  23520  discmp  23536  cmpsublem  23537  cmpsub  23538  conncompid  23569  2ndcsep  23597  cldllycmp  23633  dislly  23635  iskgen3  23687  kgencn2  23695  txuni2  23703  dfac14  23756  prdstopn  23766  txcmplem1  23779  txcmplem2  23780  hmphdis  23934  fbssfi  23975  trfbas2  23981  uffixsn  24063  hauspwpwf1  24125  alexsubALTlem2  24186  ustuqtop0  24378  met1stc  24659  restmetu  24708  icccmplem1  24961  icccmplem2  24962  opnmbllem  25741  sqff1o  27324  0lt1s  27983  oldf  28008  newf  28009  leftf  28026  rightf  28027  elons2  28429  oncutlt  28435  oniso  28442  onaddscl  28448  onmulscl  28449  onsbnd  28452  incistruhgr  29407  upgrbi  29421  umgrbi  29429  upgr1e  29441  umgredg  29466  uspgr1e  29572  uhgrspansubgrlem  29618  eupth2lems  30567  sspval  31053  foresf1o  32828  cmpcref  34218  esumpcvgval  34446  esumcvg  34454  esum2d  34461  pwsiga  34498  difelsiga  34501  sigainb  34504  pwldsys  34525  rossros  34548  measssd  34583  cntnevol  34596  ddemeas  34604  mbfmcnt  34636  br2base  34637  sxbrsigalem0  34639  oms0  34665  probun  34787  coinfliprv  34851  ballotth  34906  cvmcov2  35745  satfvel  35882  elfuns  36383  altxpsspw  36447  elhf2  36645  neibastop1  36848  neibastop2lem  36849  ctbssinf  38030  opnmbllem0  38285  heiborlem1  38440  heiborlem8  38447  pclfinN  40652  mapd1o  42400  elrfi  43405  ismrcd2  43410  istopclsd  43411  mrefg2  43418  isnacs3  43421  dfac11  43769  islssfg2  43778  lnr2i  43823  clsk1independent  44752  isotone2  44755  gneispace  44840  ismnushort  44991  trsspwALT  45506  trsspwALT2  45507  trsspwALT3  45508  pwtrVD  45512  permaxpow  45698  icof  45915  stoweidlem57  46751  intsal  47024  salexct  47028  sge0resplit  47100  sge0reuz  47141  omeiunltfirp  47213  smfpimbor1lem1  47492  sprvalpw  48206  sprsymrelf  48221  sprsymrelf1  48222  prprvalpw  48241  grimuhgr  48629  uspgropssxp  48886  uspgrsprf  48888