Theorem pweqd 4577

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  undefval  8332  pmvalg  8895  marypha1lem  9462  marypha1  9463  r1val3  9887  ackbij2lem2  10356  ackbij2lem3  10357  hfom  10360  isfin2  10411  hsmexlem8  10541  vdwmc  17200  hashbcval  17224  ismre  17810  mrcfval  17832  mrisval  17854  mreexexlemd  17868  brssc  18039  lubfval  18572  glbfval  18585  isclat  18724  issubmgm  18941  issubm  19048  issubg  19386  cntzfval  19585  lsmfval  19903  lsmpropd  19942  pj1fval  19959  issubrng  20850  issubrg  20874  rgspnval  20915  lssset  21259  lspfval  21299  lsppropd  21344  islbs  21402  sraval  21501  ocvfval  22027  isobs  22081  islinds  22170  aspval  22235  opsrval  22410  ply1frcl  22691  evls1fval  22692  basis1  23323  baspartn  23327  cldval  23396  ntrfval  23397  clsfval  23398  mretopd  23465  neifval  23472  lpfval  23511  cncls2  23646  iscnrm  23696  iscnrm2  23711  2ndcsep  23833  kgenval  23909  xkoval  23961  dfac14  23992  qtopval  24069  qtopval2  24070  isfbas  24203  trfbas2  24217  flimval  24337  elflim  24345  flimclslem  24358  fclsfnflim  24401  fclscmp  24404  tsmsfbas  24502  tsmsval2  24504  ustval  24577  utopval  24606  mopnfss  24817  setsmstopn  24852  met2ndc  24897  madeval  28275  elmade2  28301  istrkgb  28974  isuhgr  29695  isushgr  29696  isuhgrop  29705  uhgrun  29709  uhgrstrrepe  29713  isupgr  29719  upgrop  29729  isumgr  29730  upgrun  29753  umgrun  29755  isuspgr  29790  isusgr  29791  isuspgrop  29799  isusgrop  29800  ausgrusgrb  29803  usgrstrrepe  29873  issubgr  29909  uhgrspansubgrlem  29928  usgrexi  30079  1hevtxdg1  30144  umgr2v2e  30163  zarcmplem  34624  ismeas  34943  omsval  35036  omscl  35038  omsf  35039  oms0  35040  carsgval  35046  omsmeas  35066  erdszelem3  36166  erdsze  36175  kur14  36189  iscvm  36232  mpstval  36508  mclsval  36536  mh-infprim2bi  37550  bj-imdirvallem  38369  pibp21  38606  heibor  39021  idlval  39213  igenval  39261  paddfval  41120  pclfvalN  41212  polfvalN  41227  docaffvalN  42444  docafvalN  42445  djaffvalN  42456  djafvalN  42457  dochffval  42672  dochfval  42673  djhffval  42719  djhfval  42720  lpolsetN  42805  lcdlss2N  42943  mzpclval  44002  dfac21  44334  islmodfg  44337  islssfg  44338  rfovd  45262  fsovrfovd  45270  gneispace2  45393  ismnu  45506  ackbij3  46289  sge0val  47649  ismea  47734  psmeasure  47754  caragenval  47776  isome  47777  omeunile  47788  isomennd  47814  ovnval  47824  hspmbl  47912  isvonmbl  47921  afv2eq12d  48558  isisubgr  49233  isubgruhgr  49239  stgrfv  49324  stgrusgra  49330  gpgov  49413  gpgusgra  49428  lincop  49851  lcoop  49854  islininds  49889  ldepsnlinc  49951  isclatd  50428