Theorem elpw 4562

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

Syntax hints:   ↔ wb 209   ∈ wcel 2145  Vcvv 3457   ⊆ wss 3907  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-pw 4560

This theorem is referenced by:  velpw  4563  0elpw  5317  prelpw  5418  sspwb  5421  pwssun  5544  xpsspw  5787  knatar  7345  iunpw  7758  ssenen  9127  fissuni  9302  fipreima  9303  fipwuni  9374  dffi3  9379  marypha1lem  9381  inf3lem6  9590  tz9.12lem3  9749  rankonidlem  9788  r0weon  9984  infpwfien  10034  dfac5lem4  10098  dfac2b  10102  dfac12lem2  10116  enfin2i  10293  isfin1-3  10358  itunitc1  10392  hsmexlem4  10401  hsmexlem5  10402  axdc4lem  10427  pwfseqlem1  10631  eltsk2g  10724  ixxssxr  13375  ioof  13465  fzof  13675  hashbclem  14479  incexclem  15880  ramub1lem1  17076  ramub1lem2  17077  prdsplusg  17501  prdsmulr  17502  prdsvsca  17503  submrc  17674  isacs2  17699  isssc  17867  homaf  18077  catcfuccl  18165  catcxpccl  18253  clatl  18554  isacs4lem  18590  isacs5lem  18591  dprd2dlem1  20104  ablfac1b  20133  cssval  21792  tgdom  23096  distop  23113  fctop  23122  cctop  23124  ppttop  23125  pptbas  23126  epttop  23127  mretopd  23210  resttopon  23279  dishaus  23500  discmp  23516  cmpsublem  23517  cmpsub  23518  conncompid  23549  2ndcsep  23577  cldllycmp  23613  dislly  23615  iskgen3  23667  kgencn2  23675  txuni2  23683  dfac14  23736  prdstopn  23746  txcmplem1  23759  txcmplem2  23760  hmphdis  23914  fbssfi  23955  trfbas2  23961  uffixsn  24043  hauspwpwf1  24105  alexsubALTlem2  24166  ustuqtop0  24358  met1stc  24639  restmetu  24688  icccmplem1  24941  icccmplem2  24942  opnmbllem  25721  sqff1o  27304  0lt1s  27963  oldf  27988  newf  27989  leftf  28006  rightf  28007  elons2  28409  oncutlt  28415  oniso  28422  onaddscl  28428  onmulscl  28429  onsbnd  28432  incistruhgr  29338  upgrbi  29352  umgrbi  29360  upgr1e  29372  umgredg  29397  uspgr1e  29503  uhgrspansubgrlem  29549  eupth2lems  30498  sspval  30984  foresf1o  32760  cmpcref  34157  esumpcvgval  34385  esumcvg  34393  esum2d  34400  pwsiga  34437  difelsiga  34440  sigainb  34443  pwldsys  34464  rossros  34487  measssd  34522  cntnevol  34535  ddemeas  34543  mbfmcnt  34575  br2base  34576  sxbrsigalem0  34578  oms0  34604  probun  34726  coinfliprv  34790  ballotth  34845  cvmcov2  35638  satfvel  35775  elfuns  36276  altxpsspw  36340  elhf2  36538  neibastop1  36732  neibastop2lem  36733  ctbssinf  37912  opnmbllem0  38167  heiborlem1  38322  heiborlem8  38329  pclfinN  40536  mapd1o  42284  elrfi  43287  ismrcd2  43292  istopclsd  43293  mrefg2  43300  isnacs3  43303  dfac11  43651  islssfg2  43660  lnr2i  43705  clsk1independent  44634  isotone2  44637  gneispace  44722  ismnushort  44875  trsspwALT  45391  trsspwALT2  45392  trsspwALT3  45393  pwtrVD  45397  permaxpow  45583  icof  45793  stoweidlem57  46629  intsal  46902  salexct  46906  sge0resplit  46978  sge0reuz  47019  omeiunltfirp  47091  smfpimbor1lem1  47370  sprvalpw  48084  sprsymrelf  48099  sprsymrelf1  48100  prprvalpw  48119  grimuhgr  48507  uspgropssxp  48764  uspgrsprf  48766