Theorem pweqd 4558

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

Syntax hints:   → wi 4   = wceq 1537  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  undefval  7942  pmvalg  8417  marypha1lem  8897  marypha1  8898  r1val3  9267  ackbij2lem2  9662  ackbij2lem3  9663  r1om  9666  isfin2  9716  hsmexlem8  9846  vdwmc  16314  hashbcval  16338  ismre  16861  mrcfval  16879  mrisval  16901  mreexexlemd  16915  brssc  17084  lubfval  17588  glbfval  17601  isclat  17719  issubm  17968  issubg  18279  cntzfval  18450  lsmfval  18763  lsmpropd  18803  pj1fval  18820  issubrg  19535  lssset  19705  lspfval  19745  lsppropd  19790  islbs  19848  sraval  19948  aspval  20102  opsrval  20255  ply1frcl  20481  evls1fval  20482  ocvfval  20810  isobs  20864  islinds  20953  basis1  21558  baspartn  21562  cldval  21631  ntrfval  21632  clsfval  21633  mretopd  21700  neifval  21707  lpfval  21746  cncls2  21881  iscnrm  21931  iscnrm2  21946  2ndcsep  22067  kgenval  22143  xkoval  22195  dfac14  22226  qtopval  22303  qtopval2  22304  isfbas  22437  trfbas2  22451  flimval  22571  elflim  22579  flimclslem  22592  fclsfnflim  22635  fclscmp  22638  tsmsfbas  22736  tsmsval2  22738  ustval  22811  utopval  22841  mopnfss  23053  setsmstopn  23088  met2ndc  23133  istrkgb  26241  isuhgr  26845  isushgr  26846  isuhgrop  26855  uhgrun  26859  uhgrstrrepe  26863  isupgr  26869  upgrop  26879  isumgr  26880  upgrun  26903  umgrun  26905  isuspgr  26937  isusgr  26938  isuspgrop  26946  isusgrop  26947  ausgrusgrb  26950  usgrstrrepe  27017  issubgr  27053  uhgrspansubgrlem  27072  usgrexi  27223  1hevtxdg1  27288  umgr2v2e  27307  ismeas  31458  omsval  31551  omscl  31553  omsf  31554  oms0  31555  carsgval  31561  omsmeas  31581  erdszelem3  32440  erdsze  32449  kur14  32463  iscvm  32506  mpstval  32782  mclsval  32810  madeval  33289  bj-imdirval  34475  pibp21  34699  heibor  35114  idlval  35306  igenval  35354  paddfval  36948  pclfvalN  37040  polfvalN  37055  docaffvalN  38272  docafvalN  38273  djaffvalN  38284  djafvalN  38285  dochffval  38500  dochfval  38501  djhffval  38547  djhfval  38548  lpolsetN  38633  lcdlss2N  38771  mzpclval  39342  dfac21  39686  islmodfg  39689  islssfg  39690  rgspnval  39788  rfovd  40367  fsovrfovd  40375  gneispace2  40502  ismnu  40617  sge0val  42668  ismea  42753  psmeasure  42773  caragenval  42795  isome  42796  omeunile  42807  isomennd  42833  ovnval  42843  hspmbl  42931  isvonmbl  42940  afv2eq12d  43434  issubmgm  44076  lincop  44483  lcoop  44486  islininds  44521  ldepsnlinc  44583