Theorem pweqd 4568

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

Syntax hints:   → wi 4   = wceq 1540  𝒫 cpw 4551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-pw 4553

This theorem is referenced by:  undefval  8209  pmvalg  8764  marypha1lem  9323  marypha1  9324  r1val3  9734  ackbij2lem2  10133  ackbij2lem3  10134  r1om  10137  isfin2  10188  hsmexlem8  10318  vdwmc  16890  hashbcval  16914  ismre  17492  mrcfval  17514  mrisval  17536  mreexexlemd  17550  brssc  17721  lubfval  18254  glbfval  18267  isclat  18406  issubmgm  18576  issubm  18677  issubg  19005  cntzfval  19199  lsmfval  19517  lsmpropd  19556  pj1fval  19573  issubrng  20432  issubrg  20456  rgspnval  20497  lssset  20836  lspfval  20876  lsppropd  20922  islbs  20980  sraval  21079  ocvfval  21573  isobs  21627  islinds  21716  aspval  21780  opsrval  21951  ply1frcl  22203  evls1fval  22204  basis1  22835  baspartn  22839  cldval  22908  ntrfval  22909  clsfval  22910  mretopd  22977  neifval  22984  lpfval  23023  cncls2  23158  iscnrm  23208  iscnrm2  23223  2ndcsep  23344  kgenval  23420  xkoval  23472  dfac14  23503  qtopval  23580  qtopval2  23581  isfbas  23714  trfbas2  23728  flimval  23848  elflim  23856  flimclslem  23869  fclsfnflim  23912  fclscmp  23915  tsmsfbas  24013  tsmsval2  24015  ustval  24088  utopval  24118  mopnfss  24329  setsmstopn  24364  met2ndc  24409  madeval  27762  elmade2  27782  istrkgb  28400  isuhgr  29005  isushgr  29006  isuhgrop  29015  uhgrun  29019  uhgrstrrepe  29023  isupgr  29029  upgrop  29039  isumgr  29040  upgrun  29063  umgrun  29065  isuspgr  29097  isusgr  29098  isuspgrop  29106  isusgrop  29107  ausgrusgrb  29110  usgrstrrepe  29180  issubgr  29216  uhgrspansubgrlem  29235  usgrexi  29386  1hevtxdg1  29452  umgr2v2e  29471  zarcmplem  33848  ismeas  34166  omsval  34261  omscl  34263  omsf  34264  oms0  34265  carsgval  34271  omsmeas  34291  erdszelem3  35170  erdsze  35179  kur14  35193  iscvm  35236  mpstval  35512  mclsval  35540  bj-imdirvallem  37158  pibp21  37393  heibor  37805  idlval  37997  igenval  38045  paddfval  39780  pclfvalN  39872  polfvalN  39887  docaffvalN  41104  docafvalN  41105  djaffvalN  41116  djafvalN  41117  dochffval  41332  dochfval  41333  djhffval  41379  djhfval  41380  lpolsetN  41465  lcdlss2N  41603  mzpclval  42702  dfac21  43043  islmodfg  43046  islssfg  43047  rfovd  43978  fsovrfovd  43986  gneispace2  44109  ismnu  44238  sge0val  46351  ismea  46436  psmeasure  46456  caragenval  46478  isome  46479  omeunile  46490  isomennd  46516  ovnval  46526  hspmbl  46614  isvonmbl  46623  afv2eq12d  47203  isisubgr  47850  isubgruhgr  47856  stgrfv  47941  stgrusgra  47947  gpgov  48030  gpgusgra  48045  lincop  48397  lcoop  48400  islininds  48435  ldepsnlinc  48497  isclatd  48971