Theorem pweqd 4516

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 4513	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1538  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  undefval  7925  pmvalg  8400  marypha1lem  8881  marypha1  8882  r1val3  9251  ackbij2lem2  9651  ackbij2lem3  9652  r1om  9655  isfin2  9705  hsmexlem8  9835  vdwmc  16304  hashbcval  16328  ismre  16853  mrcfval  16871  mrisval  16893  mreexexlemd  16907  brssc  17076  lubfval  17580  glbfval  17593  isclat  17711  issubm  17960  issubg  18271  cntzfval  18442  lsmfval  18755  lsmpropd  18795  pj1fval  18812  issubrg  19528  lssset  19698  lspfval  19738  lsppropd  19783  islbs  19841  sraval  19941  ocvfval  20355  isobs  20409  islinds  20498  aspval  20559  opsrval  20714  ply1frcl  20942  evls1fval  20943  basis1  21555  baspartn  21559  cldval  21628  ntrfval  21629  clsfval  21630  mretopd  21697  neifval  21704  lpfval  21743  cncls2  21878  iscnrm  21928  iscnrm2  21943  2ndcsep  22064  kgenval  22140  xkoval  22192  dfac14  22223  qtopval  22300  qtopval2  22301  isfbas  22434  trfbas2  22448  flimval  22568  elflim  22576  flimclslem  22589  fclsfnflim  22632  fclscmp  22635  tsmsfbas  22733  tsmsval2  22735  ustval  22808  utopval  22838  mopnfss  23050  setsmstopn  23085  met2ndc  23130  istrkgb  26249  isuhgr  26853  isushgr  26854  isuhgrop  26863  uhgrun  26867  uhgrstrrepe  26871  isupgr  26877  upgrop  26887  isumgr  26888  upgrun  26911  umgrun  26913  isuspgr  26945  isusgr  26946  isuspgrop  26954  isusgrop  26955  ausgrusgrb  26958  usgrstrrepe  27025  issubgr  27061  uhgrspansubgrlem  27080  usgrexi  27231  1hevtxdg1  27296  umgr2v2e  27315  zarcmplem  31234  ismeas  31568  omsval  31661  omscl  31663  omsf  31664  oms0  31665  carsgval  31671  omsmeas  31691  erdszelem3  32553  erdsze  32562  kur14  32576  iscvm  32619  mpstval  32895  mclsval  32923  madeval  33402  bj-imdirvallem  34595  pibp21  34832  heibor  35259  idlval  35451  igenval  35499  paddfval  37093  pclfvalN  37185  polfvalN  37200  docaffvalN  38417  docafvalN  38418  djaffvalN  38429  djafvalN  38430  dochffval  38645  dochfval  38646  djhffval  38692  djhfval  38693  lpolsetN  38778  lcdlss2N  38916  mzpclval  39666  dfac21  40010  islmodfg  40013  islssfg  40014  rgspnval  40112  rfovd  40702  fsovrfovd  40710  gneispace2  40835  ismnu  40969  sge0val  43005  ismea  43090  psmeasure  43110  caragenval  43132  isome  43133  omeunile  43144  isomennd  43170  ovnval  43180  hspmbl  43268  isvonmbl  43277  afv2eq12d  43771  issubmgm  44409  lincop  44817  lcoop  44820  islininds  44855  ldepsnlinc  44917