Theorem pweqd 4612

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3474  df-in 3950  df-ss 3960  df-pw 4597

This theorem is referenced by:  undefval  8242  pmvalg  8813  marypha1lem  9409  marypha1  9410  r1val3  9814  ackbij2lem2  10216  ackbij2lem3  10217  r1om  10220  isfin2  10270  hsmexlem8  10400  vdwmc  16892  hashbcval  16916  ismre  17515  mrcfval  17533  mrisval  17555  mreexexlemd  17569  brssc  17742  lubfval  18284  glbfval  18297  isclat  18434  issubm  18659  issubg  18977  cntzfval  19149  lsmfval  19469  lsmpropd  19508  pj1fval  19525  issubrg  20309  lssset  20490  lspfval  20530  lsppropd  20575  islbs  20633  sraval  20735  ocvfval  21149  isobs  21205  islinds  21294  aspval  21355  opsrval  21526  ply1frcl  21763  evls1fval  21764  basis1  22379  baspartn  22383  cldval  22453  ntrfval  22454  clsfval  22455  mretopd  22522  neifval  22529  lpfval  22568  cncls2  22703  iscnrm  22753  iscnrm2  22768  2ndcsep  22889  kgenval  22965  xkoval  23017  dfac14  23048  qtopval  23125  qtopval2  23126  isfbas  23259  trfbas2  23273  flimval  23393  elflim  23401  flimclslem  23414  fclsfnflim  23457  fclscmp  23460  tsmsfbas  23558  tsmsval2  23560  ustval  23633  utopval  23663  mopnfss  23875  setsmstopn  23912  met2ndc  23958  madeval  27267  elmade2  27283  istrkgb  27568  isuhgr  28182  isushgr  28183  isuhgrop  28192  uhgrun  28196  uhgrstrrepe  28200  isupgr  28206  upgrop  28216  isumgr  28217  upgrun  28240  umgrun  28242  isuspgr  28274  isusgr  28275  isuspgrop  28283  isusgrop  28284  ausgrusgrb  28287  usgrstrrepe  28354  issubgr  28390  uhgrspansubgrlem  28409  usgrexi  28560  1hevtxdg1  28625  umgr2v2e  28644  zarcmplem  32678  ismeas  33014  omsval  33109  omscl  33111  omsf  33112  oms0  33113  carsgval  33119  omsmeas  33139  erdszelem3  34001  erdsze  34010  kur14  34024  iscvm  34067  mpstval  34343  mclsval  34371  bj-imdirvallem  35851  pibp21  36086  heibor  36480  idlval  36672  igenval  36720  paddfval  38459  pclfvalN  38551  polfvalN  38566  docaffvalN  39783  docafvalN  39784  djaffvalN  39795  djafvalN  39796  dochffval  40011  dochfval  40012  djhffval  40058  djhfval  40059  lpolsetN  40144  lcdlss2N  40282  mzpclval  41222  dfac21  41567  islmodfg  41570  islssfg  41571  rgspnval  41669  rfovd  42511  fsovrfovd  42519  gneispace2  42642  ismnu  42779  sge0val  44843  ismea  44928  psmeasure  44948  caragenval  44970  isome  44971  omeunile  44982  isomennd  45008  ovnval  45018  hspmbl  45106  isvonmbl  45115  afv2eq12d  45683  issubmgm  46319  lincop  46725  lcoop  46728  islininds  46763  ldepsnlinc  46825  isclatd  47244