Theorem elpw 4558

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-pw 4556

This theorem is referenced by:  velpw  4559  0elpw  5301  prelpw  5394  sspwb  5397  pwssun  5516  xpsspw  5758  knatar  7303  iunpw  7716  ssenen  9079  fissuni  9257  fipreima  9258  fipwuni  9329  dffi3  9334  marypha1lem  9336  inf3lem6  9542  tz9.12lem3  9701  rankonidlem  9740  r0weon  9922  infpwfien  9972  dfac5lem4  10036  dfac5lem4OLD  10038  dfac2b  10041  dfac12lem2  10055  enfin2i  10231  isfin1-3  10296  itunitc1  10330  hsmexlem4  10339  hsmexlem5  10340  axdc4lem  10365  pwfseqlem1  10569  eltsk2g  10662  ixxssxr  13273  ioof  13363  fzof  13572  hashbclem  14375  incexclem  15759  ramub1lem1  16954  ramub1lem2  16955  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  submrc  17551  isacs2  17576  isssc  17744  homaf  17954  catcfuccl  18042  catcxpccl  18130  clatl  18431  isacs4lem  18467  isacs5lem  18468  dprd2dlem1  19972  ablfac1b  20001  cssval  21637  tgdom  22922  distop  22939  fctop  22948  cctop  22950  ppttop  22951  pptbas  22952  epttop  22953  mretopd  23036  resttopon  23105  dishaus  23326  discmp  23342  cmpsublem  23343  cmpsub  23344  conncompid  23375  2ndcsep  23403  cldllycmp  23439  dislly  23441  iskgen3  23493  kgencn2  23501  txuni2  23509  dfac14  23562  prdstopn  23572  txcmplem1  23585  txcmplem2  23586  hmphdis  23740  fbssfi  23781  trfbas2  23787  uffixsn  23869  hauspwpwf1  23931  alexsubALTlem2  23992  ustuqtop0  24184  met1stc  24465  restmetu  24514  icccmplem1  24767  icccmplem2  24768  opnmbllem  25558  sqff1o  27148  0lt1s  27808  oldf  27833  newf  27834  leftf  27851  rightf  27852  elons2  28254  oncutlt  28260  oniso  28267  onaddscl  28273  onmulscl  28274  onsbnd  28277  incistruhgr  29152  upgrbi  29166  umgrbi  29174  upgr1e  29186  umgredg  29211  uspgr1e  29317  uhgrspansubgrlem  29363  eupth2lems  30313  sspval  30798  foresf1o  32579  cmpcref  34007  esumpcvgval  34235  esumcvg  34243  esum2d  34250  pwsiga  34287  difelsiga  34290  sigainb  34293  pwldsys  34314  rossros  34337  measssd  34372  cntnevol  34385  ddemeas  34393  mbfmcnt  34425  br2base  34426  sxbrsigalem0  34428  oms0  34454  probun  34576  coinfliprv  34640  ballotth  34695  cvmcov2  35469  satfvel  35606  elfuns  36107  altxpsspw  36171  elhf2  36369  neibastop1  36553  neibastop2lem  36554  ctbssinf  37607  opnmbllem0  37853  heiborlem1  38008  heiborlem8  38015  pclfinN  40156  mapd1o  41904  elrfi  42932  ismrcd2  42937  istopclsd  42938  mrefg2  42945  isnacs3  42948  dfac11  43300  islssfg2  43309  lnr2i  43354  clsk1independent  44283  isotone2  44286  gneispace  44371  ismnushort  44538  trsspwALT  45054  trsspwALT2  45055  trsspwALT3  45056  pwtrVD  45060  permaxpow  45246  icof  45459  stoweidlem57  46297  intsal  46570  salexct  46574  sge0resplit  46646  sge0reuz  46687  omeiunltfirp  46759  smfpimbor1lem1  47038  sprvalpw  47722  sprsymrelf  47737  sprsymrelf1  47738  prprvalpw  47757  grimuhgr  48129  uspgropssxp  48386  uspgrsprf  48388