Theorem pweqd 4564

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

Syntax hints:   → wi 4   = wceq 1541  𝒫 cpw 4547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-pw 4549

This theorem is referenced by:  undefval  8206  pmvalg  8761  marypha1lem  9317  marypha1  9318  r1val3  9731  ackbij2lem2  10130  ackbij2lem3  10131  r1om  10134  isfin2  10185  hsmexlem8  10315  vdwmc  16890  hashbcval  16914  ismre  17492  mrcfval  17514  mrisval  17536  mreexexlemd  17550  brssc  17721  lubfval  18254  glbfval  18267  isclat  18406  issubmgm  18610  issubm  18711  issubg  19039  cntzfval  19232  lsmfval  19550  lsmpropd  19589  pj1fval  19606  issubrng  20462  issubrg  20486  rgspnval  20527  lssset  20866  lspfval  20906  lsppropd  20952  islbs  21010  sraval  21109  ocvfval  21603  isobs  21657  islinds  21746  aspval  21810  opsrval  21981  ply1frcl  22233  evls1fval  22234  basis1  22865  baspartn  22869  cldval  22938  ntrfval  22939  clsfval  22940  mretopd  23007  neifval  23014  lpfval  23053  cncls2  23188  iscnrm  23238  iscnrm2  23253  2ndcsep  23374  kgenval  23450  xkoval  23502  dfac14  23533  qtopval  23610  qtopval2  23611  isfbas  23744  trfbas2  23758  flimval  23878  elflim  23886  flimclslem  23899  fclsfnflim  23942  fclscmp  23945  tsmsfbas  24043  tsmsval2  24045  ustval  24118  utopval  24147  mopnfss  24358  setsmstopn  24393  met2ndc  24438  madeval  27793  elmade2  27813  istrkgb  28433  isuhgr  29038  isushgr  29039  isuhgrop  29048  uhgrun  29052  uhgrstrrepe  29056  isupgr  29062  upgrop  29072  isumgr  29073  upgrun  29096  umgrun  29098  isuspgr  29130  isusgr  29131  isuspgrop  29139  isusgrop  29140  ausgrusgrb  29143  usgrstrrepe  29213  issubgr  29249  uhgrspansubgrlem  29268  usgrexi  29419  1hevtxdg1  29485  umgr2v2e  29504  zarcmplem  33894  ismeas  34212  omsval  34306  omscl  34308  omsf  34309  oms0  34310  carsgval  34316  omsmeas  34336  erdszelem3  35237  erdsze  35246  kur14  35260  iscvm  35303  mpstval  35579  mclsval  35607  bj-imdirvallem  37224  pibp21  37459  heibor  37871  idlval  38063  igenval  38111  paddfval  39906  pclfvalN  39998  polfvalN  40013  docaffvalN  41230  docafvalN  41231  djaffvalN  41242  djafvalN  41243  dochffval  41458  dochfval  41459  djhffval  41505  djhfval  41506  lpolsetN  41591  lcdlss2N  41729  mzpclval  42828  dfac21  43169  islmodfg  43172  islssfg  43173  rfovd  44104  fsovrfovd  44112  gneispace2  44235  ismnu  44364  sge0val  46474  ismea  46559  psmeasure  46579  caragenval  46601  isome  46602  omeunile  46613  isomennd  46639  ovnval  46649  hspmbl  46737  isvonmbl  46746  afv2eq12d  47325  isisubgr  47972  isubgruhgr  47978  stgrfv  48063  stgrusgra  48069  gpgov  48152  gpgusgra  48167  lincop  48519  lcoop  48522  islininds  48557  ldepsnlinc  48619  isclatd  49093