Theorem pweqd 4627

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

Syntax hints:   → wi 4   = wceq 1534  𝒫 cpw 4610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-ss 3976  df-pw 4612

This theorem is referenced by:  undefval  8299  pmvalg  8874  marypha1lem  9483  marypha1  9484  r1val3  9888  ackbij2lem2  10289  ackbij2lem3  10290  r1om  10293  isfin2  10344  hsmexlem8  10474  vdwmc  17001  hashbcval  17025  ismre  17624  mrcfval  17642  mrisval  17664  mreexexlemd  17678  brssc  17851  lubfval  18396  glbfval  18409  isclat  18546  issubmgm  18716  issubm  18814  issubg  19142  cntzfval  19336  lsmfval  19658  lsmpropd  19697  pj1fval  19714  issubrng  20551  issubrg  20577  lssset  20932  lspfval  20972  lsppropd  21018  islbs  21076  sraval  21175  ocvfval  21684  isobs  21740  islinds  21829  aspval  21892  opsrval  22075  ply1frcl  22332  evls1fval  22333  basis1  22967  baspartn  22971  cldval  23041  ntrfval  23042  clsfval  23043  mretopd  23110  neifval  23117  lpfval  23156  cncls2  23291  iscnrm  23341  iscnrm2  23356  2ndcsep  23477  kgenval  23553  xkoval  23605  dfac14  23636  qtopval  23713  qtopval2  23714  isfbas  23847  trfbas2  23861  flimval  23981  elflim  23989  flimclslem  24002  fclsfnflim  24045  fclscmp  24048  tsmsfbas  24146  tsmsval2  24148  ustval  24221  utopval  24251  mopnfss  24463  setsmstopn  24500  met2ndc  24546  madeval  27899  elmade2  27915  istrkgb  28405  isuhgr  29019  isushgr  29020  isuhgrop  29029  uhgrun  29033  uhgrstrrepe  29037  isupgr  29043  upgrop  29053  isumgr  29054  upgrun  29077  umgrun  29079  isuspgr  29111  isusgr  29112  isuspgrop  29120  isusgrop  29121  ausgrusgrb  29124  usgrstrrepe  29194  issubgr  29230  uhgrspansubgrlem  29249  usgrexi  29400  1hevtxdg1  29466  umgr2v2e  29485  zarcmplem  33734  ismeas  34070  omsval  34165  omscl  34167  omsf  34168  oms0  34169  carsgval  34175  omsmeas  34195  erdszelem3  35068  erdsze  35077  kur14  35091  iscvm  35134  mpstval  35410  mclsval  35438  bj-imdirvallem  36934  pibp21  37169  heibor  37569  idlval  37761  igenval  37809  paddfval  39543  pclfvalN  39635  polfvalN  39650  docaffvalN  40867  docafvalN  40868  djaffvalN  40879  djafvalN  40880  dochffval  41095  dochfval  41096  djhffval  41142  djhfval  41143  lpolsetN  41228  lcdlss2N  41366  mzpclval  42453  dfac21  42798  islmodfg  42801  islssfg  42802  rgspnval  42900  rfovd  43739  fsovrfovd  43747  gneispace2  43870  ismnu  44006  sge0val  46057  ismea  46142  psmeasure  46162  caragenval  46184  isome  46185  omeunile  46196  isomennd  46222  ovnval  46232  hspmbl  46320  isvonmbl  46329  afv2eq12d  46898  isisubgr  47499  isubgruhgr  47503  lincop  47872  lcoop  47875  islininds  47910  ldepsnlinc  47972  isclatd  48390