Theorem elpw 4560

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-pw 4558

This theorem is referenced by:  velpw  4561  0elpw  5303  prelpw  5401  sspwb  5404  pwssun  5524  xpsspw  5766  knatar  7313  iunpw  7726  ssenen  9091  fissuni  9269  fipreima  9270  fipwuni  9341  dffi3  9346  marypha1lem  9348  inf3lem6  9554  tz9.12lem3  9713  rankonidlem  9752  r0weon  9934  infpwfien  9984  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  dfac12lem2  10067  enfin2i  10243  isfin1-3  10308  itunitc1  10342  hsmexlem4  10351  hsmexlem5  10352  axdc4lem  10377  pwfseqlem1  10581  eltsk2g  10674  ixxssxr  13285  ioof  13375  fzof  13584  hashbclem  14387  incexclem  15771  ramub1lem1  16966  ramub1lem2  16967  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  submrc  17563  isacs2  17588  isssc  17756  homaf  17966  catcfuccl  18054  catcxpccl  18142  clatl  18443  isacs4lem  18479  isacs5lem  18480  dprd2dlem1  19984  ablfac1b  20013  cssval  21649  tgdom  22934  distop  22951  fctop  22960  cctop  22962  ppttop  22963  pptbas  22964  epttop  22965  mretopd  23048  resttopon  23117  dishaus  23338  discmp  23354  cmpsublem  23355  cmpsub  23356  conncompid  23387  2ndcsep  23415  cldllycmp  23451  dislly  23453  iskgen3  23505  kgencn2  23513  txuni2  23521  dfac14  23574  prdstopn  23584  txcmplem1  23597  txcmplem2  23598  hmphdis  23752  fbssfi  23793  trfbas2  23799  uffixsn  23881  hauspwpwf1  23943  alexsubALTlem2  24004  ustuqtop0  24196  met1stc  24477  restmetu  24526  icccmplem1  24779  icccmplem2  24780  opnmbllem  25570  sqff1o  27160  0lt1s  27820  oldf  27845  newf  27846  leftf  27863  rightf  27864  elons2  28266  oncutlt  28272  oniso  28279  onaddscl  28285  onmulscl  28286  onsbnd  28289  incistruhgr  29164  upgrbi  29178  umgrbi  29186  upgr1e  29198  umgredg  29223  uspgr1e  29329  uhgrspansubgrlem  29375  eupth2lems  30325  sspval  30810  foresf1o  32590  cmpcref  34027  esumpcvgval  34255  esumcvg  34263  esum2d  34270  pwsiga  34307  difelsiga  34310  sigainb  34313  pwldsys  34334  rossros  34357  measssd  34392  cntnevol  34405  ddemeas  34413  mbfmcnt  34445  br2base  34446  sxbrsigalem0  34448  oms0  34474  probun  34596  coinfliprv  34660  ballotth  34715  cvmcov2  35488  satfvel  35625  elfuns  36126  altxpsspw  36190  elhf2  36388  neibastop1  36572  neibastop2lem  36573  ctbssinf  37655  opnmbllem0  37901  heiborlem1  38056  heiborlem8  38063  pclfinN  40270  mapd1o  42018  elrfi  43045  ismrcd2  43050  istopclsd  43051  mrefg2  43058  isnacs3  43061  dfac11  43413  islssfg2  43422  lnr2i  43467  clsk1independent  44396  isotone2  44399  gneispace  44484  ismnushort  44651  trsspwALT  45167  trsspwALT2  45168  trsspwALT3  45169  pwtrVD  45173  permaxpow  45359  icof  45571  stoweidlem57  46409  intsal  46682  salexct  46686  sge0resplit  46758  sge0reuz  46799  omeiunltfirp  46871  smfpimbor1lem1  47150  sprvalpw  47834  sprsymrelf  47849  sprsymrelf1  47850  prprvalpw  47869  grimuhgr  48241  uspgropssxp  48498  uspgrsprf  48500