Theorem pweqd 4619

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

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

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 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  undefval  8258  pmvalg  8828  marypha1lem  9425  marypha1  9426  r1val3  9830  ackbij2lem2  10232  ackbij2lem3  10233  r1om  10236  isfin2  10286  hsmexlem8  10416  vdwmc  16908  hashbcval  16932  ismre  17531  mrcfval  17549  mrisval  17571  mreexexlemd  17585  brssc  17758  lubfval  18300  glbfval  18313  isclat  18450  issubm  18681  issubg  19001  cntzfval  19179  lsmfval  19501  lsmpropd  19540  pj1fval  19557  issubrg  20356  lssset  20537  lspfval  20577  lsppropd  20622  islbs  20680  sraval  20782  ocvfval  21211  isobs  21267  islinds  21356  aspval  21419  opsrval  21593  ply1frcl  21829  evls1fval  21830  basis1  22445  baspartn  22449  cldval  22519  ntrfval  22520  clsfval  22521  mretopd  22588  neifval  22595  lpfval  22634  cncls2  22769  iscnrm  22819  iscnrm2  22834  2ndcsep  22955  kgenval  23031  xkoval  23083  dfac14  23114  qtopval  23191  qtopval2  23192  isfbas  23325  trfbas2  23339  flimval  23459  elflim  23467  flimclslem  23480  fclsfnflim  23523  fclscmp  23526  tsmsfbas  23624  tsmsval2  23626  ustval  23699  utopval  23729  mopnfss  23941  setsmstopn  23978  met2ndc  24024  madeval  27337  elmade2  27353  istrkgb  27696  isuhgr  28310  isushgr  28311  isuhgrop  28320  uhgrun  28324  uhgrstrrepe  28328  isupgr  28334  upgrop  28344  isumgr  28345  upgrun  28368  umgrun  28370  isuspgr  28402  isusgr  28403  isuspgrop  28411  isusgrop  28412  ausgrusgrb  28415  usgrstrrepe  28482  issubgr  28518  uhgrspansubgrlem  28537  usgrexi  28688  1hevtxdg1  28753  umgr2v2e  28772  zarcmplem  32850  ismeas  33186  omsval  33281  omscl  33283  omsf  33284  oms0  33285  carsgval  33291  omsmeas  33311  erdszelem3  34173  erdsze  34182  kur14  34196  iscvm  34239  mpstval  34515  mclsval  34543  bj-imdirvallem  36050  pibp21  36285  heibor  36678  idlval  36870  igenval  36918  paddfval  38657  pclfvalN  38749  polfvalN  38764  docaffvalN  39981  docafvalN  39982  djaffvalN  39993  djafvalN  39994  dochffval  40209  dochfval  40210  djhffval  40256  djhfval  40257  lpolsetN  40342  lcdlss2N  40480  mzpclval  41449  dfac21  41794  islmodfg  41797  islssfg  41798  rgspnval  41896  rfovd  42738  fsovrfovd  42746  gneispace2  42869  ismnu  43006  sge0val  45069  ismea  45154  psmeasure  45174  caragenval  45196  isome  45197  omeunile  45208  isomennd  45234  ovnval  45244  hspmbl  45332  isvonmbl  45341  afv2eq12d  45910  issubmgm  46546  issubrng  46711  lincop  47043  lcoop  47046  islininds  47081  ldepsnlinc  47143  isclatd  47562