Theorem pweqd 4620

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

Syntax hints:   → wi 4   = wceq 1542  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  undefval  8261  pmvalg  8831  marypha1lem  9428  marypha1  9429  r1val3  9833  ackbij2lem2  10235  ackbij2lem3  10236  r1om  10239  isfin2  10289  hsmexlem8  10419  vdwmc  16911  hashbcval  16935  ismre  17534  mrcfval  17552  mrisval  17574  mreexexlemd  17588  brssc  17761  lubfval  18303  glbfval  18316  isclat  18453  issubm  18684  issubg  19006  cntzfval  19184  lsmfval  19506  lsmpropd  19545  pj1fval  19562  issubrg  20319  lssset  20544  lspfval  20584  lsppropd  20629  islbs  20687  sraval  20789  ocvfval  21219  isobs  21275  islinds  21364  aspval  21427  opsrval  21601  ply1frcl  21837  evls1fval  21838  basis1  22453  baspartn  22457  cldval  22527  ntrfval  22528  clsfval  22529  mretopd  22596  neifval  22603  lpfval  22642  cncls2  22777  iscnrm  22827  iscnrm2  22842  2ndcsep  22963  kgenval  23039  xkoval  23091  dfac14  23122  qtopval  23199  qtopval2  23200  isfbas  23333  trfbas2  23347  flimval  23467  elflim  23475  flimclslem  23488  fclsfnflim  23531  fclscmp  23534  tsmsfbas  23632  tsmsval2  23634  ustval  23707  utopval  23737  mopnfss  23949  setsmstopn  23986  met2ndc  24032  madeval  27347  elmade2  27363  istrkgb  27706  isuhgr  28320  isushgr  28321  isuhgrop  28330  uhgrun  28334  uhgrstrrepe  28338  isupgr  28344  upgrop  28354  isumgr  28355  upgrun  28378  umgrun  28380  isuspgr  28412  isusgr  28413  isuspgrop  28421  isusgrop  28422  ausgrusgrb  28425  usgrstrrepe  28492  issubgr  28528  uhgrspansubgrlem  28547  usgrexi  28698  1hevtxdg1  28763  umgr2v2e  28782  zarcmplem  32861  ismeas  33197  omsval  33292  omscl  33294  omsf  33295  oms0  33296  carsgval  33302  omsmeas  33322  erdszelem3  34184  erdsze  34193  kur14  34207  iscvm  34250  mpstval  34526  mclsval  34554  bj-imdirvallem  36061  pibp21  36296  heibor  36689  idlval  36881  igenval  36929  paddfval  38668  pclfvalN  38760  polfvalN  38775  docaffvalN  39992  docafvalN  39993  djaffvalN  40004  djafvalN  40005  dochffval  40220  dochfval  40221  djhffval  40267  djhfval  40268  lpolsetN  40353  lcdlss2N  40491  mzpclval  41463  dfac21  41808  islmodfg  41811  islssfg  41812  rgspnval  41910  rfovd  42752  fsovrfovd  42760  gneispace2  42883  ismnu  43020  sge0val  45082  ismea  45167  psmeasure  45187  caragenval  45209  isome  45210  omeunile  45221  isomennd  45247  ovnval  45257  hspmbl  45345  isvonmbl  45354  afv2eq12d  45923  issubmgm  46559  issubrng  46726  lincop  47089  lcoop  47092  islininds  47127  ldepsnlinc  47189  isclatd  47608