Theorem pweqd 4569

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

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

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-pw 4554

This theorem is referenced by:  undefval  8216  pmvalg  8772  marypha1lem  9334  marypha1  9335  r1val3  9748  ackbij2lem2  10147  ackbij2lem3  10148  r1om  10151  isfin2  10202  hsmexlem8  10332  vdwmc  16904  hashbcval  16928  ismre  17507  mrcfval  17529  mrisval  17551  mreexexlemd  17565  brssc  17736  lubfval  18269  glbfval  18282  isclat  18421  issubmgm  18625  issubm  18726  issubg  19054  cntzfval  19247  lsmfval  19565  lsmpropd  19604  pj1fval  19621  issubrng  20478  issubrg  20502  rgspnval  20543  lssset  20882  lspfval  20922  lsppropd  20968  islbs  21026  sraval  21125  ocvfval  21619  isobs  21673  islinds  21762  aspval  21826  opsrval  21999  ply1frcl  22260  evls1fval  22261  basis1  22892  baspartn  22896  cldval  22965  ntrfval  22966  clsfval  22967  mretopd  23034  neifval  23041  lpfval  23080  cncls2  23215  iscnrm  23265  iscnrm2  23280  2ndcsep  23401  kgenval  23477  xkoval  23529  dfac14  23560  qtopval  23637  qtopval2  23638  isfbas  23771  trfbas2  23785  flimval  23905  elflim  23913  flimclslem  23926  fclsfnflim  23969  fclscmp  23972  tsmsfbas  24070  tsmsval2  24072  ustval  24145  utopval  24174  mopnfss  24385  setsmstopn  24420  met2ndc  24465  madeval  27820  elmade2  27840  istrkgb  28476  isuhgr  29082  isushgr  29083  isuhgrop  29092  uhgrun  29096  uhgrstrrepe  29100  isupgr  29106  upgrop  29116  isumgr  29117  upgrun  29140  umgrun  29142  isuspgr  29174  isusgr  29175  isuspgrop  29183  isusgrop  29184  ausgrusgrb  29187  usgrstrrepe  29257  issubgr  29293  uhgrspansubgrlem  29312  usgrexi  29463  1hevtxdg1  29529  umgr2v2e  29548  zarcmplem  33987  ismeas  34305  omsval  34399  omscl  34401  omsf  34402  oms0  34403  carsgval  34409  omsmeas  34429  erdszelem3  35336  erdsze  35345  kur14  35359  iscvm  35402  mpstval  35678  mclsval  35706  bj-imdirvallem  37324  pibp21  37559  heibor  37961  idlval  38153  igenval  38201  paddfval  39996  pclfvalN  40088  polfvalN  40103  docaffvalN  41320  docafvalN  41321  djaffvalN  41332  djafvalN  41333  dochffval  41548  dochfval  41549  djhffval  41595  djhfval  41596  lpolsetN  41681  lcdlss2N  41819  mzpclval  42909  dfac21  43250  islmodfg  43253  islssfg  43254  rfovd  44184  fsovrfovd  44192  gneispace2  44315  ismnu  44444  sge0val  46552  ismea  46637  psmeasure  46657  caragenval  46679  isome  46680  omeunile  46691  isomennd  46717  ovnval  46727  hspmbl  46815  isvonmbl  46824  afv2eq12d  47403  isisubgr  48050  isubgruhgr  48056  stgrfv  48141  stgrusgra  48147  gpgov  48230  gpgusgra  48245  lincop  48596  lcoop  48599  islininds  48634  ldepsnlinc  48696  isclatd  49170