Theorem pweqd 4580

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  undefval  8255  pmvalg  8810  marypha1lem  9384  marypha1  9385  r1val3  9791  ackbij2lem2  10192  ackbij2lem3  10193  r1om  10196  isfin2  10247  hsmexlem8  10377  vdwmc  16949  hashbcval  16973  ismre  17551  mrcfval  17569  mrisval  17591  mreexexlemd  17605  brssc  17776  lubfval  18309  glbfval  18322  isclat  18459  issubmgm  18629  issubm  18730  issubg  19058  cntzfval  19252  lsmfval  19568  lsmpropd  19607  pj1fval  19624  issubrng  20456  issubrg  20480  rgspnval  20521  lssset  20839  lspfval  20879  lsppropd  20925  islbs  20983  sraval  21082  ocvfval  21575  isobs  21629  islinds  21718  aspval  21782  opsrval  21953  ply1frcl  22205  evls1fval  22206  basis1  22837  baspartn  22841  cldval  22910  ntrfval  22911  clsfval  22912  mretopd  22979  neifval  22986  lpfval  23025  cncls2  23160  iscnrm  23210  iscnrm2  23225  2ndcsep  23346  kgenval  23422  xkoval  23474  dfac14  23505  qtopval  23582  qtopval2  23583  isfbas  23716  trfbas2  23730  flimval  23850  elflim  23858  flimclslem  23871  fclsfnflim  23914  fclscmp  23917  tsmsfbas  24015  tsmsval2  24017  ustval  24090  utopval  24120  mopnfss  24331  setsmstopn  24366  met2ndc  24411  madeval  27760  elmade2  27780  istrkgb  28382  isuhgr  28987  isushgr  28988  isuhgrop  28997  uhgrun  29001  uhgrstrrepe  29005  isupgr  29011  upgrop  29021  isumgr  29022  upgrun  29045  umgrun  29047  isuspgr  29079  isusgr  29080  isuspgrop  29088  isusgrop  29089  ausgrusgrb  29092  usgrstrrepe  29162  issubgr  29198  uhgrspansubgrlem  29217  usgrexi  29368  1hevtxdg1  29434  umgr2v2e  29453  zarcmplem  33871  ismeas  34189  omsval  34284  omscl  34286  omsf  34287  oms0  34288  carsgval  34294  omsmeas  34314  erdszelem3  35180  erdsze  35189  kur14  35203  iscvm  35246  mpstval  35522  mclsval  35550  bj-imdirvallem  37168  pibp21  37403  heibor  37815  idlval  38007  igenval  38055  paddfval  39791  pclfvalN  39883  polfvalN  39898  docaffvalN  41115  docafvalN  41116  djaffvalN  41127  djafvalN  41128  dochffval  41343  dochfval  41344  djhffval  41390  djhfval  41391  lpolsetN  41476  lcdlss2N  41614  mzpclval  42713  dfac21  43055  islmodfg  43058  islssfg  43059  rfovd  43990  fsovrfovd  43998  gneispace2  44121  ismnu  44250  sge0val  46364  ismea  46449  psmeasure  46469  caragenval  46491  isome  46492  omeunile  46503  isomennd  46529  ovnval  46539  hspmbl  46627  isvonmbl  46636  afv2eq12d  47216  isisubgr  47862  isubgruhgr  47868  stgrfv  47952  stgrusgra  47958  gpgov  48033  gpgusgra  48048  lincop  48397  lcoop  48400  islininds  48435  ldepsnlinc  48497  isclatd  48971