Theorem pweqi 4582

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 4580	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 = 𝒫 𝐵

Syntax hints:   = wceq 1540  𝒫 cpw 4566

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568

This theorem is referenced by:  rankxplim  9839  pwdju1  10151  fin23lem17  10298  mnfnre  11224  qtopres  23592  hmphdis  23690  ust0  24114  made0  27792  umgrpredgv  29074  issubgr  29205  uhgrissubgr  29209  cusgredg  29358  cffldtocusgr  29381  cffldtocusgrOLD  29382  konigsbergiedgw  30184  shsspwh  31182  circtopn  33834  lfuhgr  35112  rankeq1o  36166  onsucsuccmpi  36438  bj-unirel  37046  elrfi  42689  islmodfg  43065  clsk1indlem4  44040  clsk1indlem1  44041  clsk1independent  44042  omef  46501  caragensplit  46505  caragenelss  46506  carageneld  46507  omeunile  46510  caragensspw  46514  0ome  46534  isomennd  46536  ovn02  46573  isuspgrimlem  47899  grtri  47943  usgrexmpl1lem  48016  usgrexmpl2lem  48021  lcoop  48404  lincvalsc0  48414  linc0scn0  48416  lincdifsn  48417  linc1  48418  lspsslco  48430  lincresunit3lem2  48473  lincresunit3  48474