Theorem pweqd 4583

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568

This theorem is referenced by:  undefval  8258  pmvalg  8813  marypha1lem  9391  marypha1  9392  r1val3  9798  ackbij2lem2  10199  ackbij2lem3  10200  r1om  10203  isfin2  10254  hsmexlem8  10384  vdwmc  16956  hashbcval  16980  ismre  17558  mrcfval  17576  mrisval  17598  mreexexlemd  17612  brssc  17783  lubfval  18316  glbfval  18329  isclat  18466  issubmgm  18636  issubm  18737  issubg  19065  cntzfval  19259  lsmfval  19575  lsmpropd  19614  pj1fval  19631  issubrng  20463  issubrg  20487  rgspnval  20528  lssset  20846  lspfval  20886  lsppropd  20932  islbs  20990  sraval  21089  ocvfval  21582  isobs  21636  islinds  21725  aspval  21789  opsrval  21960  ply1frcl  22212  evls1fval  22213  basis1  22844  baspartn  22848  cldval  22917  ntrfval  22918  clsfval  22919  mretopd  22986  neifval  22993  lpfval  23032  cncls2  23167  iscnrm  23217  iscnrm2  23232  2ndcsep  23353  kgenval  23429  xkoval  23481  dfac14  23512  qtopval  23589  qtopval2  23590  isfbas  23723  trfbas2  23737  flimval  23857  elflim  23865  flimclslem  23878  fclsfnflim  23921  fclscmp  23924  tsmsfbas  24022  tsmsval2  24024  ustval  24097  utopval  24127  mopnfss  24338  setsmstopn  24373  met2ndc  24418  madeval  27767  elmade2  27787  istrkgb  28389  isuhgr  28994  isushgr  28995  isuhgrop  29004  uhgrun  29008  uhgrstrrepe  29012  isupgr  29018  upgrop  29028  isumgr  29029  upgrun  29052  umgrun  29054  isuspgr  29086  isusgr  29087  isuspgrop  29095  isusgrop  29096  ausgrusgrb  29099  usgrstrrepe  29169  issubgr  29205  uhgrspansubgrlem  29224  usgrexi  29375  1hevtxdg1  29441  umgr2v2e  29460  zarcmplem  33878  ismeas  34196  omsval  34291  omscl  34293  omsf  34294  oms0  34295  carsgval  34301  omsmeas  34321  erdszelem3  35187  erdsze  35196  kur14  35210  iscvm  35253  mpstval  35529  mclsval  35557  bj-imdirvallem  37175  pibp21  37410  heibor  37822  idlval  38014  igenval  38062  paddfval  39798  pclfvalN  39890  polfvalN  39905  docaffvalN  41122  docafvalN  41123  djaffvalN  41134  djafvalN  41135  dochffval  41350  dochfval  41351  djhffval  41397  djhfval  41398  lpolsetN  41483  lcdlss2N  41621  mzpclval  42720  dfac21  43062  islmodfg  43065  islssfg  43066  rfovd  43997  fsovrfovd  44005  gneispace2  44128  ismnu  44257  sge0val  46371  ismea  46456  psmeasure  46476  caragenval  46498  isome  46499  omeunile  46510  isomennd  46536  ovnval  46546  hspmbl  46634  isvonmbl  46643  afv2eq12d  47220  isisubgr  47866  isubgruhgr  47872  stgrfv  47956  stgrusgra  47962  gpgov  48037  gpgusgra  48052  lincop  48401  lcoop  48404  islininds  48439  ldepsnlinc  48501  isclatd  48975