Theorem pweqd 4576

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

Syntax hints:   → wi 4   = wceq 1540  𝒫 cpw 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-pw 4561

This theorem is referenced by:  undefval  8232  pmvalg  8787  marypha1lem  9360  marypha1  9361  r1val3  9767  ackbij2lem2  10168  ackbij2lem3  10169  r1om  10172  isfin2  10223  hsmexlem8  10353  vdwmc  16925  hashbcval  16949  ismre  17527  mrcfval  17549  mrisval  17571  mreexexlemd  17585  brssc  17756  lubfval  18289  glbfval  18302  isclat  18441  issubmgm  18611  issubm  18712  issubg  19040  cntzfval  19234  lsmfval  19552  lsmpropd  19591  pj1fval  19608  issubrng  20467  issubrg  20491  rgspnval  20532  lssset  20871  lspfval  20911  lsppropd  20957  islbs  21015  sraval  21114  ocvfval  21608  isobs  21662  islinds  21751  aspval  21815  opsrval  21986  ply1frcl  22238  evls1fval  22239  basis1  22870  baspartn  22874  cldval  22943  ntrfval  22944  clsfval  22945  mretopd  23012  neifval  23019  lpfval  23058  cncls2  23193  iscnrm  23243  iscnrm2  23258  2ndcsep  23379  kgenval  23455  xkoval  23507  dfac14  23538  qtopval  23615  qtopval2  23616  isfbas  23749  trfbas2  23763  flimval  23883  elflim  23891  flimclslem  23904  fclsfnflim  23947  fclscmp  23950  tsmsfbas  24048  tsmsval2  24050  ustval  24123  utopval  24153  mopnfss  24364  setsmstopn  24399  met2ndc  24444  madeval  27797  elmade2  27817  istrkgb  28435  isuhgr  29040  isushgr  29041  isuhgrop  29050  uhgrun  29054  uhgrstrrepe  29058  isupgr  29064  upgrop  29074  isumgr  29075  upgrun  29098  umgrun  29100  isuspgr  29132  isusgr  29133  isuspgrop  29141  isusgrop  29142  ausgrusgrb  29145  usgrstrrepe  29215  issubgr  29251  uhgrspansubgrlem  29270  usgrexi  29421  1hevtxdg1  29487  umgr2v2e  29506  zarcmplem  33864  ismeas  34182  omsval  34277  omscl  34279  omsf  34280  oms0  34281  carsgval  34287  omsmeas  34307  erdszelem3  35173  erdsze  35182  kur14  35196  iscvm  35239  mpstval  35515  mclsval  35543  bj-imdirvallem  37161  pibp21  37396  heibor  37808  idlval  38000  igenval  38048  paddfval  39784  pclfvalN  39876  polfvalN  39891  docaffvalN  41108  docafvalN  41109  djaffvalN  41120  djafvalN  41121  dochffval  41336  dochfval  41337  djhffval  41383  djhfval  41384  lpolsetN  41469  lcdlss2N  41607  mzpclval  42706  dfac21  43048  islmodfg  43051  islssfg  43052  rfovd  43983  fsovrfovd  43991  gneispace2  44114  ismnu  44243  sge0val  46357  ismea  46442  psmeasure  46462  caragenval  46484  isome  46485  omeunile  46496  isomennd  46522  ovnval  46532  hspmbl  46620  isvonmbl  46629  afv2eq12d  47209  isisubgr  47855  isubgruhgr  47861  stgrfv  47945  stgrusgra  47951  gpgov  48026  gpgusgra  48041  lincop  48390  lcoop  48393  islininds  48428  ldepsnlinc  48490  isclatd  48964