Theorem pweqd 4572

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-pw 4557

This theorem is referenced by:  undefval  8220  pmvalg  8778  marypha1lem  9340  marypha1  9341  r1val3  9754  ackbij2lem2  10153  ackbij2lem3  10154  r1om  10157  isfin2  10208  hsmexlem8  10338  vdwmc  16910  hashbcval  16934  ismre  17513  mrcfval  17535  mrisval  17557  mreexexlemd  17571  brssc  17742  lubfval  18275  glbfval  18288  isclat  18427  issubmgm  18631  issubm  18732  issubg  19060  cntzfval  19253  lsmfval  19571  lsmpropd  19610  pj1fval  19627  issubrng  20484  issubrg  20508  rgspnval  20549  lssset  20888  lspfval  20928  lsppropd  20974  islbs  21032  sraval  21131  ocvfval  21625  isobs  21679  islinds  21768  aspval  21832  opsrval  22005  ply1frcl  22266  evls1fval  22267  basis1  22898  baspartn  22902  cldval  22971  ntrfval  22972  clsfval  22973  mretopd  23040  neifval  23047  lpfval  23086  cncls2  23221  iscnrm  23271  iscnrm2  23286  2ndcsep  23407  kgenval  23483  xkoval  23535  dfac14  23566  qtopval  23643  qtopval2  23644  isfbas  23777  trfbas2  23791  flimval  23911  elflim  23919  flimclslem  23932  fclsfnflim  23975  fclscmp  23978  tsmsfbas  24076  tsmsval2  24078  ustval  24151  utopval  24180  mopnfss  24391  setsmstopn  24426  met2ndc  24471  madeval  27830  elmade2  27850  istrkgb  28510  isuhgr  29116  isushgr  29117  isuhgrop  29126  uhgrun  29130  uhgrstrrepe  29134  isupgr  29140  upgrop  29150  isumgr  29151  upgrun  29174  umgrun  29176  isuspgr  29208  isusgr  29209  isuspgrop  29217  isusgrop  29218  ausgrusgrb  29221  usgrstrrepe  29291  issubgr  29327  uhgrspansubgrlem  29346  usgrexi  29497  1hevtxdg1  29563  umgr2v2e  29582  zarcmplem  34019  ismeas  34337  omsval  34431  omscl  34433  omsf  34434  oms0  34435  carsgval  34441  omsmeas  34461  erdszelem3  35368  erdsze  35377  kur14  35391  iscvm  35434  mpstval  35710  mclsval  35738  bj-imdirvallem  37356  pibp21  37591  heibor  37993  idlval  38185  igenval  38233  paddfval  40094  pclfvalN  40186  polfvalN  40201  docaffvalN  41418  docafvalN  41419  djaffvalN  41430  djafvalN  41431  dochffval  41646  dochfval  41647  djhffval  41693  djhfval  41694  lpolsetN  41779  lcdlss2N  41917  mzpclval  43003  dfac21  43344  islmodfg  43347  islssfg  43348  rfovd  44278  fsovrfovd  44286  gneispace2  44409  ismnu  44538  sge0val  46646  ismea  46731  psmeasure  46751  caragenval  46773  isome  46774  omeunile  46785  isomennd  46811  ovnval  46821  hspmbl  46909  isvonmbl  46918  afv2eq12d  47497  isisubgr  48144  isubgruhgr  48150  stgrfv  48235  stgrusgra  48241  gpgov  48324  gpgusgra  48339  lincop  48690  lcoop  48693  islininds  48728  ldepsnlinc  48790  isclatd  49264