Theorem pweqd 4621

Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)

Hypothesis

Ref	Expression
pweqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
pweqd	⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweqd

Step	Hyp	Ref	Expression
1		pweqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		pweq 4618	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1536  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-pw 4606

This theorem is referenced by:  undefval  8299  pmvalg  8875  marypha1lem  9470  marypha1  9471  r1val3  9875  ackbij2lem2  10276  ackbij2lem3  10277  r1om  10280  isfin2  10331  hsmexlem8  10461  vdwmc  17011  hashbcval  17035  ismre  17634  mrcfval  17652  mrisval  17674  mreexexlemd  17688  brssc  17861  lubfval  18407  glbfval  18420  isclat  18557  issubmgm  18727  issubm  18828  issubg  19156  cntzfval  19350  lsmfval  19670  lsmpropd  19709  pj1fval  19726  issubrng  20563  issubrg  20587  rgspnval  20628  lssset  20948  lspfval  20988  lsppropd  21034  islbs  21092  sraval  21191  ocvfval  21701  isobs  21757  islinds  21846  aspval  21910  opsrval  22081  ply1frcl  22337  evls1fval  22338  basis1  22972  baspartn  22976  cldval  23046  ntrfval  23047  clsfval  23048  mretopd  23115  neifval  23122  lpfval  23161  cncls2  23296  iscnrm  23346  iscnrm2  23361  2ndcsep  23482  kgenval  23558  xkoval  23610  dfac14  23641  qtopval  23718  qtopval2  23719  isfbas  23852  trfbas2  23866  flimval  23986  elflim  23994  flimclslem  24007  fclsfnflim  24050  fclscmp  24053  tsmsfbas  24151  tsmsval2  24153  ustval  24226  utopval  24256  mopnfss  24468  setsmstopn  24505  met2ndc  24551  madeval  27905  elmade2  27921  istrkgb  28477  isuhgr  29091  isushgr  29092  isuhgrop  29101  uhgrun  29105  uhgrstrrepe  29109  isupgr  29115  upgrop  29125  isumgr  29126  upgrun  29149  umgrun  29151  isuspgr  29183  isusgr  29184  isuspgrop  29192  isusgrop  29193  ausgrusgrb  29196  usgrstrrepe  29266  issubgr  29302  uhgrspansubgrlem  29321  usgrexi  29472  1hevtxdg1  29538  umgr2v2e  29557  zarcmplem  33841  ismeas  34179  omsval  34274  omscl  34276  omsf  34277  oms0  34278  carsgval  34284  omsmeas  34304  erdszelem3  35177  erdsze  35186  kur14  35200  iscvm  35243  mpstval  35519  mclsval  35547  bj-imdirvallem  37162  pibp21  37397  heibor  37807  idlval  37999  igenval  38047  paddfval  39779  pclfvalN  39871  polfvalN  39886  docaffvalN  41103  docafvalN  41104  djaffvalN  41115  djafvalN  41116  dochffval  41331  dochfval  41332  djhffval  41378  djhfval  41379  lpolsetN  41464  lcdlss2N  41602  mzpclval  42712  dfac21  43054  islmodfg  43057  islssfg  43058  rfovd  43990  fsovrfovd  43998  gneispace2  44121  ismnu  44256  sge0val  46321  ismea  46406  psmeasure  46426  caragenval  46448  isome  46449  omeunile  46460  isomennd  46486  ovnval  46496  hspmbl  46584  isvonmbl  46593  afv2eq12d  47164  isisubgr  47785  isubgruhgr  47791  stgrfv  47855  stgrusgra  47861  gpgov  47936  gpgusgra  47946  lincop  48253  lcoop  48256  islininds  48291  ldepsnlinc  48353  isclatd  48771