Theorem elpw 4537

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  velpw  4538  0elpw  5278  snelpwi  5360  snelpw  5361  prelpw  5362  sspwb  5365  pwssun  5485  xpsspw  5719  knatar  7228  iunpw  7621  ssenen  8938  fissuni  9124  fipreima  9125  fipwuni  9185  dffi3  9190  marypha1lem  9192  inf3lem6  9391  tz9.12lem3  9547  rankonidlem  9586  r0weon  9768  infpwfien  9818  dfac5lem4  9882  dfac2b  9886  dfac12lem2  9900  enfin2i  10077  isfin1-3  10142  itunitc1  10176  hsmexlem4  10185  hsmexlem5  10186  axdc4lem  10211  pwfseqlem1  10414  eltsk2g  10507  ixxssxr  13091  ioof  13179  fzof  13384  hashbclem  14164  incexclem  15548  ramub1lem1  16727  ramub1lem2  16728  prdsplusg  17169  prdsmulr  17170  prdsvsca  17171  submrc  17337  isacs2  17362  isssc  17532  homaf  17745  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  clatl  18226  isacs4lem  18262  isacs5lem  18263  dprd2dlem1  19644  ablfac1b  19673  cssval  20887  tgdom  22128  distop  22145  fctop  22154  cctop  22156  ppttop  22157  pptbas  22158  epttop  22159  mretopd  22243  resttopon  22312  dishaus  22533  discmp  22549  cmpsublem  22550  cmpsub  22551  conncompid  22582  2ndcsep  22610  cldllycmp  22646  dislly  22648  iskgen3  22700  kgencn2  22708  txuni2  22716  dfac14  22769  prdstopn  22779  txcmplem1  22792  txcmplem2  22793  hmphdis  22947  fbssfi  22988  trfbas2  22994  uffixsn  23076  hauspwpwf1  23138  alexsubALTlem2  23199  ustuqtop0  23392  met1stc  23677  restmetu  23726  icccmplem1  23985  icccmplem2  23986  opnmbllem  24765  sqff1o  26331  incistruhgr  27449  upgrbi  27463  umgrbi  27471  upgr1e  27483  umgredg  27508  uspgr1e  27611  uhgrspansubgrlem  27657  eupth2lems  28602  sspval  29085  foresf1o  30850  cmpcref  31800  esumpcvgval  32046  esumcvg  32054  esum2d  32061  pwsiga  32098  difelsiga  32101  sigainb  32104  pwldsys  32125  rossros  32148  measssd  32183  cntnevol  32196  ddemeas  32204  mbfmcnt  32235  br2base  32236  sxbrsigalem0  32238  oms0  32264  probun  32386  coinfliprv  32449  ballotth  32504  cvmcov2  33237  satfvel  33374  0slt1s  34023  oldf  34041  newf  34042  leftf  34049  rightf  34050  elfuns  34217  altxpsspw  34279  elhf2  34477  neibastop1  34548  neibastop2lem  34549  ctbssinf  35577  opnmbllem0  35813  heiborlem1  35969  heiborlem8  35976  pclfinN  37914  mapd1o  39662  elrfi  40516  ismrcd2  40521  istopclsd  40522  mrefg2  40529  isnacs3  40532  dfac11  40887  islssfg2  40896  lnr2i  40941  clsk1independent  41656  isotone2  41659  gneispace  41744  ismnushort  41919  trsspwALT  42438  trsspwALT2  42439  trsspwALT3  42440  pwtrVD  42444  icof  42759  stoweidlem57  43598  intsal  43869  salexct  43873  sge0resplit  43944  sge0reuz  43985  omeiunltfirp  44057  smfpimbor1lem1  44332  sprvalpw  44932  sprsymrelf  44947  sprsymrelf1  44948  prprvalpw  44967  uspgropssxp  45306  uspgrsprf  45308