Theorem elpw 4545

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

Syntax hints:   ↔ wb 208   ∈ wcel 2114  Vcvv 3496   ⊆ wss 3938  𝒫 cpw 4541

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  velpw  4546  0elpw  5258  snelpwi  5339  snelpw  5340  prelpw  5341  sspwb  5344  pwssun  5458  xpsspw  5684  knatar  7112  iunpw  7495  ssenen  8693  fissuni  8831  fipreima  8832  fipwuni  8892  dffi3  8897  marypha1lem  8899  inf3lem6  9098  tz9.12lem3  9220  rankonidlem  9259  r0weon  9440  infpwfien  9490  dfac5lem4  9554  dfac2b  9558  dfac12lem2  9572  enfin2i  9745  isfin1-3  9810  itunitc1  9844  hsmexlem4  9853  hsmexlem5  9854  axdc4lem  9879  pwfseqlem1  10082  eltsk2g  10175  ixxssxr  12753  ioof  12838  fzof  13038  hashbclem  13813  incexclem  15193  ramub1lem1  16364  ramub1lem2  16365  prdsplusg  16733  prdsmulr  16734  prdsvsca  16735  submrc  16901  isacs2  16926  isssc  17092  homaf  17292  catcfuccl  17371  catcxpccl  17459  clatl  17728  isacs4lem  17780  isacs5lem  17781  dprd2dlem1  19165  ablfac1b  19194  cssval  20828  tgdom  21588  distop  21605  fctop  21614  cctop  21616  ppttop  21617  pptbas  21618  epttop  21619  mretopd  21702  resttopon  21771  dishaus  21992  discmp  22008  cmpsublem  22009  cmpsub  22010  conncompid  22041  2ndcsep  22069  cldllycmp  22105  dislly  22107  iskgen3  22159  kgencn2  22167  txuni2  22175  dfac14  22228  prdstopn  22238  txcmplem1  22251  txcmplem2  22252  hmphdis  22406  fbssfi  22447  trfbas2  22453  uffixsn  22535  hauspwpwf1  22597  alexsubALTlem2  22658  ustuqtop0  22851  met1stc  23133  restmetu  23182  icccmplem1  23432  icccmplem2  23433  opnmbllem  24204  sqff1o  25761  incistruhgr  26866  upgrbi  26880  umgrbi  26888  upgr1e  26900  umgredg  26925  uspgr1e  27028  uhgrspansubgrlem  27074  eupth2lems  28019  sspval  28502  foresf1o  30267  cmpcref  31116  esumpcvgval  31339  esumcvg  31347  esum2d  31354  pwsiga  31391  difelsiga  31394  sigainb  31397  inelpisys  31415  pwldsys  31418  rossros  31441  measssd  31476  cntnevol  31489  ddemeas  31497  mbfmcnt  31528  br2base  31529  sxbrsigalem0  31531  oms0  31557  probun  31679  coinfliprv  31742  ballotth  31797  cvmcov2  32524  satfvel  32661  elfuns  33378  altxpsspw  33440  elhf2  33638  neibastop1  33709  neibastop2lem  33710  ctbssinf  34689  opnmbllem0  34930  heiborlem1  35091  heiborlem8  35098  pclfinN  37038  mapd1o  38786  elrfi  39298  ismrcd2  39303  istopclsd  39304  mrefg2  39311  isnacs3  39314  dfac11  39669  islssfg2  39678  lnr2i  39723  clsk1independent  40403  isotone2  40406  gneispace  40491  trsspwALT  41159  trsspwALT2  41160  trsspwALT3  41161  pwtrVD  41165  icof  41489  stoweidlem57  42349  intsal  42620  salexct  42624  sge0resplit  42695  sge0reuz  42736  omeiunltfirp  42808  smfpimbor1lem1  43080  sprvalpw  43649  sprsymrelf  43664  sprsymrelf1  43665  prprvalpw  43684  uspgropssxp  44026  uspgrsprf  44028