Theorem elpw 4534

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  velpw  4535  0elpw  5273  snelpwi  5354  snelpw  5355  prelpw  5356  sspwb  5359  pwssun  5476  xpsspw  5708  knatar  7208  iunpw  7599  ssenen  8887  fissuni  9054  fipreima  9055  fipwuni  9115  dffi3  9120  marypha1lem  9122  inf3lem6  9321  tz9.12lem3  9478  rankonidlem  9517  r0weon  9699  infpwfien  9749  dfac5lem4  9813  dfac2b  9817  dfac12lem2  9831  enfin2i  10008  isfin1-3  10073  itunitc1  10107  hsmexlem4  10116  hsmexlem5  10117  axdc4lem  10142  pwfseqlem1  10345  eltsk2g  10438  ixxssxr  13020  ioof  13108  fzof  13313  hashbclem  14092  incexclem  15476  ramub1lem1  16655  ramub1lem2  16656  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  submrc  17254  isacs2  17279  isssc  17449  homaf  17661  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  clatl  18141  isacs4lem  18177  isacs5lem  18178  dprd2dlem1  19559  ablfac1b  19588  cssval  20799  tgdom  22036  distop  22053  fctop  22062  cctop  22064  ppttop  22065  pptbas  22066  epttop  22067  mretopd  22151  resttopon  22220  dishaus  22441  discmp  22457  cmpsublem  22458  cmpsub  22459  conncompid  22490  2ndcsep  22518  cldllycmp  22554  dislly  22556  iskgen3  22608  kgencn2  22616  txuni2  22624  dfac14  22677  prdstopn  22687  txcmplem1  22700  txcmplem2  22701  hmphdis  22855  fbssfi  22896  trfbas2  22902  uffixsn  22984  hauspwpwf1  23046  alexsubALTlem2  23107  ustuqtop0  23300  met1stc  23583  restmetu  23632  icccmplem1  23891  icccmplem2  23892  opnmbllem  24670  sqff1o  26236  incistruhgr  27352  upgrbi  27366  umgrbi  27374  upgr1e  27386  umgredg  27411  uspgr1e  27514  uhgrspansubgrlem  27560  eupth2lems  28503  sspval  28986  foresf1o  30751  cmpcref  31702  esumpcvgval  31946  esumcvg  31954  esum2d  31961  pwsiga  31998  difelsiga  32001  sigainb  32004  pwldsys  32025  rossros  32048  measssd  32083  cntnevol  32096  ddemeas  32104  mbfmcnt  32135  br2base  32136  sxbrsigalem0  32138  oms0  32164  probun  32286  coinfliprv  32349  ballotth  32404  cvmcov2  33137  satfvel  33274  0slt1s  33950  oldf  33968  newf  33969  leftf  33976  rightf  33977  elfuns  34144  altxpsspw  34206  elhf2  34404  neibastop1  34475  neibastop2lem  34476  ctbssinf  35504  opnmbllem0  35740  heiborlem1  35896  heiborlem8  35903  pclfinN  37841  mapd1o  39589  elrfi  40432  ismrcd2  40437  istopclsd  40438  mrefg2  40445  isnacs3  40448  dfac11  40803  islssfg2  40812  lnr2i  40857  clsk1independent  41545  isotone2  41548  gneispace  41633  ismnushort  41808  trsspwALT  42327  trsspwALT2  42328  trsspwALT3  42329  pwtrVD  42333  icof  42648  stoweidlem57  43488  intsal  43759  salexct  43763  sge0resplit  43834  sge0reuz  43875  omeiunltfirp  43947  smfpimbor1lem1  44219  sprvalpw  44820  sprsymrelf  44835  sprsymrelf1  44836  prprvalpw  44855  uspgropssxp  45194  uspgrsprf  45196