Theorem elpw 4608

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

Syntax hints:   ↔ wb 206   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-pw 4606

This theorem is referenced by:  velpw  4609  0elpw  5361  snelpwiOLD  5454  prelpw  5456  sspwb  5459  pwssun  5579  xpsspw  5821  knatar  7376  iunpw  7789  ssenen  9189  fissuni  9394  fipreima  9395  fipwuni  9463  dffi3  9468  marypha1lem  9470  inf3lem6  9670  tz9.12lem3  9826  rankonidlem  9865  r0weon  10049  infpwfien  10099  dfac5lem4  10163  dfac5lem4OLD  10165  dfac2b  10168  dfac12lem2  10182  enfin2i  10358  isfin1-3  10423  itunitc1  10457  hsmexlem4  10466  hsmexlem5  10467  axdc4lem  10492  pwfseqlem1  10695  eltsk2g  10788  ixxssxr  13395  ioof  13483  fzof  13692  hashbclem  14487  incexclem  15868  ramub1lem1  17059  ramub1lem2  17060  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  submrc  17672  isacs2  17697  isssc  17867  homaf  18083  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  clatl  18565  isacs4lem  18601  isacs5lem  18602  dprd2dlem1  20075  ablfac1b  20104  cssval  21717  tgdom  23000  distop  23017  fctop  23026  cctop  23028  ppttop  23029  pptbas  23030  epttop  23031  mretopd  23115  resttopon  23184  dishaus  23405  discmp  23421  cmpsublem  23422  cmpsub  23423  conncompid  23454  2ndcsep  23482  cldllycmp  23518  dislly  23520  iskgen3  23572  kgencn2  23580  txuni2  23588  dfac14  23641  prdstopn  23651  txcmplem1  23664  txcmplem2  23665  hmphdis  23819  fbssfi  23860  trfbas2  23866  uffixsn  23948  hauspwpwf1  24010  alexsubALTlem2  24071  ustuqtop0  24264  met1stc  24549  restmetu  24598  icccmplem1  24857  icccmplem2  24858  opnmbllem  25649  sqff1o  27239  0slt1s  27888  oldf  27910  newf  27911  leftf  27918  rightf  27919  elons2  28295  onaddscl  28300  onmulscl  28301  incistruhgr  29110  upgrbi  29124  umgrbi  29132  upgr1e  29144  umgredg  29169  uspgr1e  29275  uhgrspansubgrlem  29321  eupth2lems  30266  sspval  30751  foresf1o  32531  cmpcref  33810  esumpcvgval  34058  esumcvg  34066  esum2d  34073  pwsiga  34110  difelsiga  34113  sigainb  34116  pwldsys  34137  rossros  34160  measssd  34195  cntnevol  34208  ddemeas  34216  mbfmcnt  34249  br2base  34250  sxbrsigalem0  34252  oms0  34278  probun  34400  coinfliprv  34463  ballotth  34518  cvmcov2  35259  satfvel  35396  elfuns  35896  altxpsspw  35958  elhf2  36156  neibastop1  36341  neibastop2lem  36342  ctbssinf  37388  opnmbllem0  37642  heiborlem1  37797  heiborlem8  37804  pclfinN  39882  mapd1o  41630  elrfi  42681  ismrcd2  42686  istopclsd  42687  mrefg2  42694  isnacs3  42697  dfac11  43050  islssfg2  43059  lnr2i  43104  clsk1independent  44035  isotone2  44038  gneispace  44123  ismnushort  44296  trsspwALT  44815  trsspwALT2  44816  trsspwALT3  44817  pwtrVD  44821  icof  45161  stoweidlem57  46012  intsal  46285  salexct  46289  sge0resplit  46361  sge0reuz  46402  omeiunltfirp  46474  smfpimbor1lem1  46753  sprvalpw  47404  sprsymrelf  47419  sprsymrelf1  47420  prprvalpw  47439  grimuhgr  47815  uspgropssxp  47987  uspgrsprf  47989