Theorem pweqd 4383

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

Syntax hints:   → wi 4   = wceq 1658  𝒫 cpw 4378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812  df-pw 4380

This theorem is referenced by:  undefval  7667  pmvalg  8133  marypha1lem  8608  marypha1  8609  r1val3  8978  ackbij2lem2  9377  ackbij2lem3  9378  r1om  9381  isfin2  9431  hsmexlem8  9561  vdwmc  16053  hashbcval  16077  ismre  16603  mrcfval  16621  mrisval  16643  mreexexlemd  16657  brssc  16826  lubfval  17331  glbfval  17344  isclat  17462  issubm  17700  issubg  17945  cntzfval  18103  symgval  18149  lsmfval  18404  lsmpropd  18441  pj1fval  18458  issubrg  19136  lssset  19290  lspfval  19332  lsppropd  19377  islbs  19435  sraval  19537  aspval  19689  opsrval  19835  ply1frcl  20043  evls1fval  20044  ocvfval  20373  isobs  20427  islinds  20515  basis1  21125  baspartn  21129  cldval  21198  ntrfval  21199  clsfval  21200  mretopd  21267  neifval  21274  lpfval  21313  cncls2  21448  iscnrm  21498  iscnrm2  21513  2ndcsep  21633  kgenval  21709  xkoval  21761  dfac14  21792  qtopval  21869  qtopval2  21870  isfbas  22003  trfbas2  22017  flimval  22137  elflim  22145  flimclslem  22158  fclsfnflim  22201  fclscmp  22204  tsmsfbas  22301  tsmsval2  22303  ustval  22376  utopval  22406  mopnfss  22618  setsmstopn  22653  met2ndc  22698  istrkgb  25767  isuhgr  26358  isushgr  26359  isuhgrop  26368  uhgrun  26372  uhgrstrrepe  26376  isupgr  26382  upgrop  26392  isumgr  26393  upgrun  26416  umgrun  26418  isuspgr  26451  isusgr  26452  isuspgrop  26460  isusgrop  26461  ausgrusgrb  26464  usgrstrrepe  26532  issubgr  26568  uhgrspansubgrlem  26587  usgrexi  26739  1hevtxdg1  26804  umgr2v2e  26823  ismeas  30807  omsval  30900  omscl  30902  omsf  30903  oms0  30904  carsgval  30910  omsmeas  30930  erdszelem3  31721  erdsze  31730  kur14  31744  iscvm  31787  mpstval  31978  mclsval  32006  madeval  32474  heibor  34162  idlval  34354  igenval  34402  paddfval  35872  pclfvalN  35964  polfvalN  35979  docaffvalN  37196  docafvalN  37197  djaffvalN  37208  djafvalN  37209  dochffval  37424  dochfval  37425  djhffval  37471  djhfval  37472  lpolsetN  37557  lcdlss2N  37695  mzpclval  38132  dfac21  38479  islmodfg  38482  islssfg  38483  rgspnval  38581  rfovd  39135  fsovrfovd  39143  gneispace2  39270  sge0val  41374  ismea  41459  psmeasure  41479  caragenval  41501  isome  41502  omeunile  41513  isomennd  41539  ovnval  41549  hspmbl  41637  isvonmbl  41646  afv2eq12d  42117  issubmgm  42636  lincop  43044  lcoop  43047  islininds  43082  ldepsnlinc  43144