Theorem pweqd 4573

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  undefval  8228  pmvalg  8786  marypha1lem  9348  marypha1  9349  r1val3  9762  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  isfin2  10216  hsmexlem8  10346  vdwmc  16918  hashbcval  16942  ismre  17521  mrcfval  17543  mrisval  17565  mreexexlemd  17579  brssc  17750  lubfval  18283  glbfval  18296  isclat  18435  issubmgm  18639  issubm  18740  issubg  19068  cntzfval  19261  lsmfval  19579  lsmpropd  19618  pj1fval  19635  issubrng  20492  issubrg  20516  rgspnval  20557  lssset  20896  lspfval  20936  lsppropd  20982  islbs  21040  sraval  21139  ocvfval  21633  isobs  21687  islinds  21776  aspval  21840  opsrval  22013  ply1frcl  22274  evls1fval  22275  basis1  22906  baspartn  22910  cldval  22979  ntrfval  22980  clsfval  22981  mretopd  23048  neifval  23055  lpfval  23094  cncls2  23229  iscnrm  23279  iscnrm2  23294  2ndcsep  23415  kgenval  23491  xkoval  23543  dfac14  23574  qtopval  23651  qtopval2  23652  isfbas  23785  trfbas2  23799  flimval  23919  elflim  23927  flimclslem  23940  fclsfnflim  23983  fclscmp  23986  tsmsfbas  24084  tsmsval2  24086  ustval  24159  utopval  24188  mopnfss  24399  setsmstopn  24434  met2ndc  24479  madeval  27840  elmade2  27866  istrkgb  28539  isuhgr  29145  isushgr  29146  isuhgrop  29155  uhgrun  29159  uhgrstrrepe  29163  isupgr  29169  upgrop  29179  isumgr  29180  upgrun  29203  umgrun  29205  isuspgr  29237  isusgr  29238  isuspgrop  29246  isusgrop  29247  ausgrusgrb  29250  usgrstrrepe  29320  issubgr  29356  uhgrspansubgrlem  29375  usgrexi  29526  1hevtxdg1  29592  umgr2v2e  29611  zarcmplem  34059  ismeas  34377  omsval  34471  omscl  34473  omsf  34474  oms0  34475  carsgval  34481  omsmeas  34501  erdszelem3  35409  erdsze  35418  kur14  35432  iscvm  35475  mpstval  35751  mclsval  35779  bj-imdirvallem  37435  pibp21  37670  heibor  38072  idlval  38264  igenval  38312  paddfval  40173  pclfvalN  40265  polfvalN  40280  docaffvalN  41497  docafvalN  41498  djaffvalN  41509  djafvalN  41510  dochffval  41725  dochfval  41726  djhffval  41772  djhfval  41773  lpolsetN  41858  lcdlss2N  41996  mzpclval  43082  dfac21  43423  islmodfg  43426  islssfg  43427  rfovd  44357  fsovrfovd  44365  gneispace2  44488  ismnu  44617  sge0val  46724  ismea  46809  psmeasure  46829  caragenval  46851  isome  46852  omeunile  46863  isomennd  46889  ovnval  46899  hspmbl  46987  isvonmbl  46996  afv2eq12d  47575  isisubgr  48222  isubgruhgr  48228  stgrfv  48313  stgrusgra  48319  gpgov  48402  gpgusgra  48417  lincop  48768  lcoop  48771  islininds  48806  ldepsnlinc  48868  isclatd  49342