Theorem pweqd 4504

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

Syntax hints:   → wi 4   = wceq 1542  𝒫 cpw 4485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-pw 4487

This theorem is referenced by:  undefval  7964  pmvalg  8441  marypha1lem  8963  marypha1  8964  r1val3  9333  ackbij2lem2  9733  ackbij2lem3  9734  r1om  9737  isfin2  9787  hsmexlem8  9917  vdwmc  16407  hashbcval  16431  ismre  16957  mrcfval  16975  mrisval  16997  mreexexlemd  17011  brssc  17182  lubfval  17697  glbfval  17710  isclat  17828  issubm  18077  issubg  18390  cntzfval  18561  lsmfval  18874  lsmpropd  18914  pj1fval  18931  issubrg  19647  lssset  19817  lspfval  19857  lsppropd  19902  islbs  19960  sraval  20060  ocvfval  20475  isobs  20529  islinds  20618  aspval  20679  opsrval  20850  ply1frcl  21081  evls1fval  21082  basis1  21694  baspartn  21698  cldval  21767  ntrfval  21768  clsfval  21769  mretopd  21836  neifval  21843  lpfval  21882  cncls2  22017  iscnrm  22067  iscnrm2  22082  2ndcsep  22203  kgenval  22279  xkoval  22331  dfac14  22362  qtopval  22439  qtopval2  22440  isfbas  22573  trfbas2  22587  flimval  22707  elflim  22715  flimclslem  22728  fclsfnflim  22771  fclscmp  22774  tsmsfbas  22872  tsmsval2  22874  ustval  22947  utopval  22977  mopnfss  23189  setsmstopn  23224  met2ndc  23269  istrkgb  26393  isuhgr  26997  isushgr  26998  isuhgrop  27007  uhgrun  27011  uhgrstrrepe  27015  isupgr  27021  upgrop  27031  isumgr  27032  upgrun  27055  umgrun  27057  isuspgr  27089  isusgr  27090  isuspgrop  27098  isusgrop  27099  ausgrusgrb  27102  usgrstrrepe  27169  issubgr  27205  uhgrspansubgrlem  27224  usgrexi  27375  1hevtxdg1  27440  umgr2v2e  27459  zarcmplem  31395  ismeas  31729  omsval  31822  omscl  31824  omsf  31825  oms0  31826  carsgval  31832  omsmeas  31852  erdszelem3  32718  erdsze  32727  kur14  32741  iscvm  32784  mpstval  33060  mclsval  33088  madeval  33669  elmade2  33681  bj-imdirvallem  34961  pibp21  35198  heibor  35591  idlval  35783  igenval  35831  paddfval  37423  pclfvalN  37515  polfvalN  37530  docaffvalN  38747  docafvalN  38748  djaffvalN  38759  djafvalN  38760  dochffval  38975  dochfval  38976  djhffval  39022  djhfval  39023  lpolsetN  39108  lcdlss2N  39246  mzpclval  40103  dfac21  40447  islmodfg  40450  islssfg  40451  rgspnval  40549  rfovd  41139  fsovrfovd  41147  gneispace2  41272  ismnu  41405  sge0val  43430  ismea  43515  psmeasure  43535  caragenval  43557  isome  43558  omeunile  43569  isomennd  43595  ovnval  43605  hspmbl  43693  isvonmbl  43702  afv2eq12d  44224  issubmgm  44861  lincop  45267  lcoop  45270  islininds  45305  ldepsnlinc  45367