Theorem pweqd 4592

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-pw 4577

This theorem is referenced by:  undefval  8273  pmvalg  8849  marypha1lem  9443  marypha1  9444  r1val3  9850  ackbij2lem2  10251  ackbij2lem3  10252  r1om  10255  isfin2  10306  hsmexlem8  10436  vdwmc  16996  hashbcval  17020  ismre  17600  mrcfval  17618  mrisval  17640  mreexexlemd  17654  brssc  17825  lubfval  18358  glbfval  18371  isclat  18508  issubmgm  18678  issubm  18779  issubg  19107  cntzfval  19301  lsmfval  19617  lsmpropd  19656  pj1fval  19673  issubrng  20505  issubrg  20529  rgspnval  20570  lssset  20888  lspfval  20928  lsppropd  20974  islbs  21032  sraval  21131  ocvfval  21624  isobs  21678  islinds  21767  aspval  21831  opsrval  22002  ply1frcl  22254  evls1fval  22255  basis1  22886  baspartn  22890  cldval  22959  ntrfval  22960  clsfval  22961  mretopd  23028  neifval  23035  lpfval  23074  cncls2  23209  iscnrm  23259  iscnrm2  23274  2ndcsep  23395  kgenval  23471  xkoval  23523  dfac14  23554  qtopval  23631  qtopval2  23632  isfbas  23765  trfbas2  23779  flimval  23899  elflim  23907  flimclslem  23920  fclsfnflim  23963  fclscmp  23966  tsmsfbas  24064  tsmsval2  24066  ustval  24139  utopval  24169  mopnfss  24380  setsmstopn  24415  met2ndc  24460  madeval  27808  elmade2  27824  istrkgb  28380  isuhgr  28985  isushgr  28986  isuhgrop  28995  uhgrun  28999  uhgrstrrepe  29003  isupgr  29009  upgrop  29019  isumgr  29020  upgrun  29043  umgrun  29045  isuspgr  29077  isusgr  29078  isuspgrop  29086  isusgrop  29087  ausgrusgrb  29090  usgrstrrepe  29160  issubgr  29196  uhgrspansubgrlem  29215  usgrexi  29366  1hevtxdg1  29432  umgr2v2e  29451  zarcmplem  33858  ismeas  34176  omsval  34271  omscl  34273  omsf  34274  oms0  34275  carsgval  34281  omsmeas  34301  erdszelem3  35161  erdsze  35170  kur14  35184  iscvm  35227  mpstval  35503  mclsval  35531  bj-imdirvallem  37144  pibp21  37379  heibor  37791  idlval  37983  igenval  38031  paddfval  39762  pclfvalN  39854  polfvalN  39869  docaffvalN  41086  docafvalN  41087  djaffvalN  41098  djafvalN  41099  dochffval  41314  dochfval  41315  djhffval  41361  djhfval  41362  lpolsetN  41447  lcdlss2N  41585  mzpclval  42695  dfac21  43037  islmodfg  43040  islssfg  43041  rfovd  43972  fsovrfovd  43980  gneispace2  44103  ismnu  44233  sge0val  46343  ismea  46428  psmeasure  46448  caragenval  46470  isome  46471  omeunile  46482  isomennd  46508  ovnval  46518  hspmbl  46606  isvonmbl  46615  afv2eq12d  47192  isisubgr  47823  isubgruhgr  47829  stgrfv  47913  stgrusgra  47919  gpgov  47994  gpgusgra  48009  lincop  48332  lcoop  48335  islininds  48370  ldepsnlinc  48432  isclatd  48905