Theorem pweqd 4571

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

Syntax hints:   → wi 4   = wceq 1541  𝒫 cpw 4554

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556

This theorem is referenced by:  undefval  8218  pmvalg  8774  marypha1lem  9336  marypha1  9337  r1val3  9750  ackbij2lem2  10149  ackbij2lem3  10150  r1om  10153  isfin2  10204  hsmexlem8  10334  vdwmc  16906  hashbcval  16930  ismre  17509  mrcfval  17531  mrisval  17553  mreexexlemd  17567  brssc  17738  lubfval  18271  glbfval  18284  isclat  18423  issubmgm  18627  issubm  18728  issubg  19056  cntzfval  19249  lsmfval  19567  lsmpropd  19606  pj1fval  19623  issubrng  20480  issubrg  20504  rgspnval  20545  lssset  20884  lspfval  20924  lsppropd  20970  islbs  21028  sraval  21127  ocvfval  21621  isobs  21675  islinds  21764  aspval  21828  opsrval  22001  ply1frcl  22262  evls1fval  22263  basis1  22894  baspartn  22898  cldval  22967  ntrfval  22968  clsfval  22969  mretopd  23036  neifval  23043  lpfval  23082  cncls2  23217  iscnrm  23267  iscnrm2  23282  2ndcsep  23403  kgenval  23479  xkoval  23531  dfac14  23562  qtopval  23639  qtopval2  23640  isfbas  23773  trfbas2  23787  flimval  23907  elflim  23915  flimclslem  23928  fclsfnflim  23971  fclscmp  23974  tsmsfbas  24072  tsmsval2  24074  ustval  24147  utopval  24176  mopnfss  24387  setsmstopn  24422  met2ndc  24467  madeval  27828  elmade2  27854  istrkgb  28527  isuhgr  29133  isushgr  29134  isuhgrop  29143  uhgrun  29147  uhgrstrrepe  29151  isupgr  29157  upgrop  29167  isumgr  29168  upgrun  29191  umgrun  29193  isuspgr  29225  isusgr  29226  isuspgrop  29234  isusgrop  29235  ausgrusgrb  29238  usgrstrrepe  29308  issubgr  29344  uhgrspansubgrlem  29363  usgrexi  29514  1hevtxdg1  29580  umgr2v2e  29599  zarcmplem  34038  ismeas  34356  omsval  34450  omscl  34452  omsf  34453  oms0  34454  carsgval  34460  omsmeas  34480  erdszelem3  35387  erdsze  35396  kur14  35410  iscvm  35453  mpstval  35729  mclsval  35757  bj-imdirvallem  37385  pibp21  37620  heibor  38022  idlval  38214  igenval  38262  paddfval  40067  pclfvalN  40159  polfvalN  40174  docaffvalN  41391  docafvalN  41392  djaffvalN  41403  djafvalN  41404  dochffval  41619  dochfval  41620  djhffval  41666  djhfval  41667  lpolsetN  41752  lcdlss2N  41890  mzpclval  42977  dfac21  43318  islmodfg  43321  islssfg  43322  rfovd  44252  fsovrfovd  44260  gneispace2  44383  ismnu  44512  sge0val  46620  ismea  46705  psmeasure  46725  caragenval  46747  isome  46748  omeunile  46759  isomennd  46785  ovnval  46795  hspmbl  46883  isvonmbl  46892  afv2eq12d  47471  isisubgr  48118  isubgruhgr  48124  stgrfv  48209  stgrusgra  48215  gpgov  48298  gpgusgra  48313  lincop  48664  lcoop  48667  islininds  48702  ldepsnlinc  48764  isclatd  49238