Theorem pweqi 4579

Description: Equality inference for power class. (Contributed by NM, 27-Nov-2013.)

Hypothesis

Ref	Expression
pweqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
pweqi	⊢ 𝒫 𝐴 = 𝒫 𝐵

Proof of Theorem pweqi

Step	Hyp	Ref	Expression
1		pweqi.1	. 2 ⊢ 𝐴 = 𝐵
2		pweq 4577	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 = 𝒫 𝐵

Syntax hints:   = wceq 1540  𝒫 cpw 4563

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 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  rankxplim  9832  pwdju1  10144  fin23lem17  10291  mnfnre  11217  qtopres  23585  hmphdis  23683  ust0  24107  made0  27785  umgrpredgv  29067  issubgr  29198  uhgrissubgr  29202  cusgredg  29351  cffldtocusgr  29374  cffldtocusgrOLD  29375  konigsbergiedgw  30177  shsspwh  31175  circtopn  33827  lfuhgr  35105  rankeq1o  36159  onsucsuccmpi  36431  bj-unirel  37039  elrfi  42682  islmodfg  43058  clsk1indlem4  44033  clsk1indlem1  44034  clsk1independent  44035  omef  46494  caragensplit  46498  caragenelss  46499  carageneld  46500  omeunile  46503  caragensspw  46507  0ome  46527  isomennd  46529  ovn02  46566  isuspgrimlem  47895  grtri  47939  usgrexmpl1lem  48012  usgrexmpl2lem  48017  lcoop  48400  lincvalsc0  48410  linc0scn0  48412  lincdifsn  48413  linc1  48414  lspsslco  48426  lincresunit3lem2  48469  lincresunit3  48470