Theorem pweqd 4581

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-pw 4566

This theorem is used by:  undefval  8279  pmvalg  8840  marypha1lem  9400  marypha1  9401  r1val3  9817  ackbij2lem2  10238  ackbij2lem3  10239  r1om  10242  isfin2  10293  hsmexlem8  10423  vdwmc  17062  hashbcval  17086  ismre  17666  mrcfval  17688  mrisval  17710  mreexexlemd  17724  brssc  17895  lubfval  18428  glbfval  18441  isclat  18580  issubmgm  18794  issubm  18900  issubg  19238  cntzfval  19436  lsmfval  19754  lsmpropd  19793  pj1fval  19810  issubrng  20698  issubrg  20722  rgspnval  20763  lssset  21106  lspfval  21146  lsppropd  21191  islbs  21249  sraval  21348  ocvfval  21868  isobs  21922  islinds  22011  aspval  22074  opsrval  22249  ply1frcl  22530  evls1fval  22531  basis1  23159  baspartn  23163  cldval  23232  ntrfval  23233  clsfval  23234  mretopd  23301  neifval  23308  lpfval  23347  cncls2  23482  iscnrm  23532  iscnrm2  23547  2ndcsep  23669  kgenval  23745  xkoval  23797  dfac14  23828  qtopval  23905  qtopval2  23906  isfbas  24039  trfbas2  24053  flimval  24173  elflim  24181  flimclslem  24194  fclsfnflim  24237  fclscmp  24240  tsmsfbas  24338  tsmsval2  24340  ustval  24413  utopval  24442  mopnfss  24653  setsmstopn  24688  met2ndc  24733  madeval  28078  elmade2  28104  istrkgb  28777  isuhgr  29467  isushgr  29468  isuhgrop  29477  uhgrun  29481  uhgrstrrepe  29485  isupgr  29491  upgrop  29501  isumgr  29502  upgrun  29525  umgrun  29527  isuspgr  29562  isusgr  29563  isuspgrop  29571  isusgrop  29572  ausgrusgrb  29575  usgrstrrepe  29645  issubgr  29681  uhgrspansubgrlem  29700  usgrexi  29851  1hevtxdg1  29916  umgr2v2e  29935  zarcmplem  34337  ismeas  34656  omsval  34750  omscl  34752  omsf  34753  oms0  34754  carsgval  34760  omsmeas  34780  erdszelem3  35724  erdsze  35733  kur14  35747  iscvm  35790  mpstval  36066  mclsval  36094  mh-infprim2bi  37117  bj-imdirvallem  37883  pibp21  38120  heibor  38532  idlval  38724  igenval  38772  paddfval  40631  pclfvalN  40723  polfvalN  40738  docaffvalN  41955  docafvalN  41956  djaffvalN  41967  djafvalN  41968  dochffval  42183  dochfval  42184  djhffval  42230  djhfval  42231  lpolsetN  42316  lcdlss2N  42454  mzpclval  43516  dfac21  43853  islmodfg  43856  islssfg  43857  rfovd  44787  fsovrfovd  44795  gneispace2  44918  ismnu  45031  sge0val  47140  ismea  47225  psmeasure  47245  caragenval  47267  isome  47268  omeunile  47279  isomennd  47305  ovnval  47315  hspmbl  47403  isvonmbl  47412  afv2eq12d  48012  isisubgr  48687  isubgruhgr  48693  stgrfv  48778  stgrusgra  48784  gpgov  48867  gpgusgra  48882  lincop  49247  lcoop  49250  islininds  49285  ldepsnlinc  49347  isclatd  49820