Theorem elpw 4557

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3438   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3922  df-pw 4555

This theorem is referenced by:  velpw  4558  0elpw  5298  snelpwiOLD  5391  prelpw  5393  sspwb  5396  pwssun  5515  xpsspw  5756  knatar  7298  iunpw  7711  ssenen  9075  fissuni  9266  fipreima  9267  fipwuni  9335  dffi3  9340  marypha1lem  9342  inf3lem6  9548  tz9.12lem3  9704  rankonidlem  9743  r0weon  9925  infpwfien  9975  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  dfac12lem2  10058  enfin2i  10234  isfin1-3  10299  itunitc1  10333  hsmexlem4  10342  hsmexlem5  10343  axdc4lem  10368  pwfseqlem1  10571  eltsk2g  10664  ixxssxr  13278  ioof  13368  fzof  13577  hashbclem  14377  incexclem  15761  ramub1lem1  16956  ramub1lem2  16957  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  submrc  17552  isacs2  17577  isssc  17745  homaf  17955  catcfuccl  18043  catcxpccl  18131  clatl  18432  isacs4lem  18468  isacs5lem  18469  dprd2dlem1  19940  ablfac1b  19969  cssval  21607  tgdom  22881  distop  22898  fctop  22907  cctop  22909  ppttop  22910  pptbas  22911  epttop  22912  mretopd  22995  resttopon  23064  dishaus  23285  discmp  23301  cmpsublem  23302  cmpsub  23303  conncompid  23334  2ndcsep  23362  cldllycmp  23398  dislly  23400  iskgen3  23452  kgencn2  23460  txuni2  23468  dfac14  23521  prdstopn  23531  txcmplem1  23544  txcmplem2  23545  hmphdis  23699  fbssfi  23740  trfbas2  23746  uffixsn  23828  hauspwpwf1  23890  alexsubALTlem2  23951  ustuqtop0  24144  met1stc  24425  restmetu  24474  icccmplem1  24727  icccmplem2  24728  opnmbllem  25518  sqff1o  27108  0slt1s  27761  oldf  27785  newf  27786  leftf  27797  rightf  27798  elons2  28182  onscutlt  28188  onsiso  28192  onaddscl  28197  onmulscl  28198  incistruhgr  29042  upgrbi  29056  umgrbi  29064  upgr1e  29076  umgredg  29101  uspgr1e  29207  uhgrspansubgrlem  29253  eupth2lems  30200  sspval  30685  foresf1o  32466  cmpcref  33816  esumpcvgval  34044  esumcvg  34052  esum2d  34059  pwsiga  34096  difelsiga  34099  sigainb  34102  pwldsys  34123  rossros  34146  measssd  34181  cntnevol  34194  ddemeas  34202  mbfmcnt  34235  br2base  34236  sxbrsigalem0  34238  oms0  34264  probun  34386  coinfliprv  34450  ballotth  34505  cvmcov2  35247  satfvel  35384  elfuns  35888  altxpsspw  35950  elhf2  36148  neibastop1  36332  neibastop2lem  36333  ctbssinf  37379  opnmbllem0  37635  heiborlem1  37790  heiborlem8  37797  pclfinN  39879  mapd1o  41627  elrfi  42667  ismrcd2  42672  istopclsd  42673  mrefg2  42680  isnacs3  42683  dfac11  43035  islssfg2  43044  lnr2i  43089  clsk1independent  44019  isotone2  44022  gneispace  44107  ismnushort  44274  trsspwALT  44791  trsspwALT2  44792  trsspwALT3  44793  pwtrVD  44797  permaxpow  44983  icof  45197  stoweidlem57  46039  intsal  46312  salexct  46316  sge0resplit  46388  sge0reuz  46429  omeiunltfirp  46501  smfpimbor1lem1  46780  sprvalpw  47465  sprsymrelf  47480  sprsymrelf1  47481  prprvalpw  47500  grimuhgr  47872  uspgropssxp  48129  uspgrsprf  48131