Theorem pweqd 4639

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

Syntax hints:   → wi 4   = wceq 1537  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  undefval  8317  pmvalg  8895  marypha1lem  9502  marypha1  9503  r1val3  9907  ackbij2lem2  10308  ackbij2lem3  10309  r1om  10312  isfin2  10363  hsmexlem8  10493  vdwmc  17025  hashbcval  17049  ismre  17648  mrcfval  17666  mrisval  17688  mreexexlemd  17702  brssc  17875  lubfval  18420  glbfval  18433  isclat  18570  issubmgm  18740  issubm  18838  issubg  19166  cntzfval  19360  lsmfval  19680  lsmpropd  19719  pj1fval  19736  issubrng  20573  issubrg  20599  lssset  20954  lspfval  20994  lsppropd  21040  islbs  21098  sraval  21197  ocvfval  21707  isobs  21763  islinds  21852  aspval  21916  opsrval  22087  ply1frcl  22343  evls1fval  22344  basis1  22978  baspartn  22982  cldval  23052  ntrfval  23053  clsfval  23054  mretopd  23121  neifval  23128  lpfval  23167  cncls2  23302  iscnrm  23352  iscnrm2  23367  2ndcsep  23488  kgenval  23564  xkoval  23616  dfac14  23647  qtopval  23724  qtopval2  23725  isfbas  23858  trfbas2  23872  flimval  23992  elflim  24000  flimclslem  24013  fclsfnflim  24056  fclscmp  24059  tsmsfbas  24157  tsmsval2  24159  ustval  24232  utopval  24262  mopnfss  24474  setsmstopn  24511  met2ndc  24557  madeval  27909  elmade2  27925  istrkgb  28481  isuhgr  29095  isushgr  29096  isuhgrop  29105  uhgrun  29109  uhgrstrrepe  29113  isupgr  29119  upgrop  29129  isumgr  29130  upgrun  29153  umgrun  29155  isuspgr  29187  isusgr  29188  isuspgrop  29196  isusgrop  29197  ausgrusgrb  29200  usgrstrrepe  29270  issubgr  29306  uhgrspansubgrlem  29325  usgrexi  29476  1hevtxdg1  29542  umgr2v2e  29561  zarcmplem  33827  ismeas  34163  omsval  34258  omscl  34260  omsf  34261  oms0  34262  carsgval  34268  omsmeas  34288  erdszelem3  35161  erdsze  35170  kur14  35184  iscvm  35227  mpstval  35503  mclsval  35531  bj-imdirvallem  37146  pibp21  37381  heibor  37781  idlval  37973  igenval  38021  paddfval  39754  pclfvalN  39846  polfvalN  39861  docaffvalN  41078  docafvalN  41079  djaffvalN  41090  djafvalN  41091  dochffval  41306  dochfval  41307  djhffval  41353  djhfval  41354  lpolsetN  41439  lcdlss2N  41577  mzpclval  42681  dfac21  43023  islmodfg  43026  islssfg  43027  rgspnval  43125  rfovd  43963  fsovrfovd  43971  gneispace2  44094  ismnu  44230  sge0val  46287  ismea  46372  psmeasure  46392  caragenval  46414  isome  46415  omeunile  46426  isomennd  46452  ovnval  46462  hspmbl  46550  isvonmbl  46559  afv2eq12d  47130  isisubgr  47734  isubgruhgr  47738  lincop  48137  lcoop  48140  islininds  48175  ldepsnlinc  48237  isclatd  48655