Theorem elpw 4546

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  velpw  4547  0elpw  5293  prelpw  5393  sspwb  5396  pwssun  5516  xpsspw  5758  knatar  7305  iunpw  7718  ssenen  9082  fissuni  9260  fipreima  9261  fipwuni  9332  dffi3  9337  marypha1lem  9339  inf3lem6  9545  tz9.12lem3  9704  rankonidlem  9743  r0weon  9925  infpwfien  9975  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  dfac12lem2  10058  enfin2i  10234  isfin1-3  10299  itunitc1  10333  hsmexlem4  10342  hsmexlem5  10343  axdc4lem  10368  pwfseqlem1  10572  eltsk2g  10665  ixxssxr  13301  ioof  13391  fzof  13601  hashbclem  14405  incexclem  15792  ramub1lem1  16988  ramub1lem2  16989  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  submrc  17585  isacs2  17610  isssc  17778  homaf  17988  catcfuccl  18076  catcxpccl  18164  clatl  18465  isacs4lem  18501  isacs5lem  18502  dprd2dlem1  20009  ablfac1b  20038  cssval  21672  tgdom  22953  distop  22970  fctop  22979  cctop  22981  ppttop  22982  pptbas  22983  epttop  22984  mretopd  23067  resttopon  23136  dishaus  23357  discmp  23373  cmpsublem  23374  cmpsub  23375  conncompid  23406  2ndcsep  23434  cldllycmp  23470  dislly  23472  iskgen3  23524  kgencn2  23532  txuni2  23540  dfac14  23593  prdstopn  23603  txcmplem1  23616  txcmplem2  23617  hmphdis  23771  fbssfi  23812  trfbas2  23818  uffixsn  23900  hauspwpwf1  23962  alexsubALTlem2  24023  ustuqtop0  24215  met1stc  24496  restmetu  24545  icccmplem1  24798  icccmplem2  24799  opnmbllem  25578  sqff1o  27159  0lt1s  27818  oldf  27843  newf  27844  leftf  27861  rightf  27862  elons2  28264  oncutlt  28270  oniso  28277  onaddscl  28283  onmulscl  28284  onsbnd  28287  incistruhgr  29162  upgrbi  29176  umgrbi  29184  upgr1e  29196  umgredg  29221  uspgr1e  29327  uhgrspansubgrlem  29373  eupth2lems  30323  sspval  30809  foresf1o  32589  cmpcref  34010  esumpcvgval  34238  esumcvg  34246  esum2d  34253  pwsiga  34290  difelsiga  34293  sigainb  34296  pwldsys  34317  rossros  34340  measssd  34375  cntnevol  34388  ddemeas  34396  mbfmcnt  34428  br2base  34429  sxbrsigalem0  34431  oms0  34457  probun  34579  coinfliprv  34643  ballotth  34698  cvmcov2  35473  satfvel  35610  elfuns  36111  altxpsspw  36175  elhf2  36373  neibastop1  36557  neibastop2lem  36558  ctbssinf  37736  opnmbllem0  37991  heiborlem1  38146  heiborlem8  38153  pclfinN  40360  mapd1o  42108  elrfi  43140  ismrcd2  43145  istopclsd  43146  mrefg2  43153  isnacs3  43156  dfac11  43508  islssfg2  43517  lnr2i  43562  clsk1independent  44491  isotone2  44494  gneispace  44579  ismnushort  44746  trsspwALT  45262  trsspwALT2  45263  trsspwALT3  45264  pwtrVD  45268  permaxpow  45454  icof  45666  stoweidlem57  46503  intsal  46776  salexct  46780  sge0resplit  46852  sge0reuz  46893  omeiunltfirp  46965  smfpimbor1lem1  47244  sprvalpw  47952  sprsymrelf  47967  sprsymrelf1  47968  prprvalpw  47987  grimuhgr  48375  uspgropssxp  48632  uspgrsprf  48634