Theorem pweqd 4617

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602

This theorem is referenced by:  undefval  8301  pmvalg  8877  marypha1lem  9473  marypha1  9474  r1val3  9878  ackbij2lem2  10279  ackbij2lem3  10280  r1om  10283  isfin2  10334  hsmexlem8  10464  vdwmc  17016  hashbcval  17040  ismre  17633  mrcfval  17651  mrisval  17673  mreexexlemd  17687  brssc  17858  lubfval  18395  glbfval  18408  isclat  18545  issubmgm  18715  issubm  18816  issubg  19144  cntzfval  19338  lsmfval  19656  lsmpropd  19695  pj1fval  19712  issubrng  20547  issubrg  20571  rgspnval  20612  lssset  20931  lspfval  20971  lsppropd  21017  islbs  21075  sraval  21174  ocvfval  21684  isobs  21740  islinds  21829  aspval  21893  opsrval  22064  ply1frcl  22322  evls1fval  22323  basis1  22957  baspartn  22961  cldval  23031  ntrfval  23032  clsfval  23033  mretopd  23100  neifval  23107  lpfval  23146  cncls2  23281  iscnrm  23331  iscnrm2  23346  2ndcsep  23467  kgenval  23543  xkoval  23595  dfac14  23626  qtopval  23703  qtopval2  23704  isfbas  23837  trfbas2  23851  flimval  23971  elflim  23979  flimclslem  23992  fclsfnflim  24035  fclscmp  24038  tsmsfbas  24136  tsmsval2  24138  ustval  24211  utopval  24241  mopnfss  24453  setsmstopn  24490  met2ndc  24536  madeval  27891  elmade2  27907  istrkgb  28463  isuhgr  29077  isushgr  29078  isuhgrop  29087  uhgrun  29091  uhgrstrrepe  29095  isupgr  29101  upgrop  29111  isumgr  29112  upgrun  29135  umgrun  29137  isuspgr  29169  isusgr  29170  isuspgrop  29178  isusgrop  29179  ausgrusgrb  29182  usgrstrrepe  29252  issubgr  29288  uhgrspansubgrlem  29307  usgrexi  29458  1hevtxdg1  29524  umgr2v2e  29543  zarcmplem  33880  ismeas  34200  omsval  34295  omscl  34297  omsf  34298  oms0  34299  carsgval  34305  omsmeas  34325  erdszelem3  35198  erdsze  35207  kur14  35221  iscvm  35264  mpstval  35540  mclsval  35568  bj-imdirvallem  37181  pibp21  37416  heibor  37828  idlval  38020  igenval  38068  paddfval  39799  pclfvalN  39891  polfvalN  39906  docaffvalN  41123  docafvalN  41124  djaffvalN  41135  djafvalN  41136  dochffval  41351  dochfval  41352  djhffval  41398  djhfval  41399  lpolsetN  41484  lcdlss2N  41622  mzpclval  42736  dfac21  43078  islmodfg  43081  islssfg  43082  rfovd  44014  fsovrfovd  44022  gneispace2  44145  ismnu  44280  sge0val  46381  ismea  46466  psmeasure  46486  caragenval  46508  isome  46509  omeunile  46520  isomennd  46546  ovnval  46556  hspmbl  46644  isvonmbl  46653  afv2eq12d  47227  isisubgr  47848  isubgruhgr  47854  stgrfv  47920  stgrusgra  47926  gpgov  48001  gpgusgra  48012  lincop  48325  lcoop  48328  islininds  48363  ldepsnlinc  48425  isclatd  48872