Theorem elpw 4561

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3451   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-pw 4559

This theorem is used by:  velpw  4562  0elpw  5317  prelpw  5414  sspwb  5417  pwssun  5543  xpsspw  5787  knatar  7359  iunpw  7774  ssenen  9154  fissuni  9330  fipreima  9331  fipwuni  9402  dffi3  9407  marypha1lem  9409  inf3lem6  9618  tz9.12lem3  9779  rankonidlem  9819  elhf2  9891  r0weon  10072  infpwfien  10122  dfac5lem4  10186  dfac2b  10190  dfac12lem2  10204  enfin2i  10380  isfin1-3  10445  itunitc1  10479  hsmexlem4  10488  hsmexlem5  10489  axdc4lem  10514  pwfseqlem1  10724  eltsk2g  10817  ixxssxr  13469  ioof  13559  fzof  13770  hashbclem  14577  incexclem  15985  ramub1lem1  17184  ramub1lem2  17185  prdsplusg  17609  prdsmulr  17610  prdsvsca  17611  submrc  17782  isacs2  17807  isssc  17975  homaf  18185  catcfuccl  18273  catcxpccl  18361  clatl  18662  isacs4lem  18698  isacs5lem  18699  dprd2dlem1  20237  ablfac1b  20266  cssval  21968  tgdom  23276  distop  23293  fctop  23302  cctop  23304  ppttop  23305  pptbas  23306  epttop  23307  mretopd  23390  resttopon  23459  dishaus  23680  discmp  23696  cmpsublem  23697  cmpsub  23698  conncompid  23729  2ndcsep  23758  cldllycmp  23794  dislly  23796  iskgen3  23848  kgencn2  23856  txuni2  23864  dfac14  23917  prdstopn  23927  txcmplem1  23940  txcmplem2  23941  hmphdis  24095  fbssfi  24136  trfbas2  24142  uffixsn  24224  hauspwpwf1  24286  alexsubALTlem2  24347  ustuqtop0  24539  met1stc  24820  restmetu  24869  icccmplem1  25122  icccmplem2  25123  opnmbllem  25902  sqff1o  27491  0lt1s  28180  oldf  28205  newf  28206  leftf  28223  rightf  28224  elons2  28626  oncutlt  28632  oniso  28639  onaddscl  28645  onmulscl  28646  onsbnd  28649  incistruhgr  29639  upgrbi  29653  umgrbi  29661  upgr1e  29673  umgredg  29698  uspgr1e  29807  uhgrspansubgrlem  29853  eupth2lems  30821  sspval  31307  foresf1o  33082  cmpcref  34464  esumpcvgval  34692  esumcvg  34700  esum2d  34707  pwsiga  34744  sigainb  34751  pwldsys  34772  rossros  34795  measssd  34830  cntnevol  34843  ddemeas  34851  mbfmcnt  34883  br2base  34884  sxbrsigalem0  34886  oms0  34912  probun  35034  coinfliprv  35098  ballotth  35153  cvmcov2  36009  satfvel  36146  elfuns  36647  altxpsspw  36712  neibastop1  37117  neibastop2lem  37118  ctbssinf  38297  opnmbllem0  38542  heiborlem1  38713  heiborlem8  38720  pclfinN  40925  mapd1o  42673  elrfi  43658  ismrcd2  43663  istopclsd  43664  mrefg2  43671  isnacs3  43674  dfac11  44022  islssfg2  44031  lnr2i  44076  clsk1independent  45005  isotone2  45008  gneispace  45093  ismnushort  45244  trsspwALT  45759  trsspwALT2  45760  trsspwALT3  45761  pwtrVD  45765  permaxpow  45951  icof  46175  stoweidlem57  47011  intsal  47284  salexct  47288  sge0resplit  47360  sge0reuz  47401  omeiunltfirp  47473  smfpimbor1lem1  47752  sprvalpw  48506  sprsymrelf  48521  sprsymrelf1  48522  prprvalpw  48541  grimuhgr  48929  uspgropssxp  49186  uspgrsprf  49188