Theorem pweqi 4568

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

Syntax hints:   = wceq 1541  𝒫 cpw 4552

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-pw 4554

This theorem is referenced by:  rankxplim  9789  pwdju1  10099  fin23lem17  10246  mnfnre  11173  qtopres  23640  hmphdis  23738  ust0  24162  made0  27845  umgrpredgv  29162  issubgr  29293  uhgrissubgr  29297  cusgredg  29446  cffldtocusgr  29469  cffldtocusgrOLD  29470  konigsbergiedgw  30272  shsspwh  31270  circtopn  33943  r11  35199  r12  35200  lfuhgr  35261  rankeq1o  36314  onsucsuccmpi  36586  bj-unirel  37195  elrfi  42878  islmodfg  43253  clsk1indlem4  44227  clsk1indlem1  44228  clsk1independent  44229  omef  46682  caragensplit  46686  caragenelss  46687  carageneld  46688  omeunile  46691  caragensspw  46695  0ome  46715  isomennd  46717  ovn02  46754  isuspgrimlem  48083  grtri  48128  usgrexmpl1lem  48209  usgrexmpl2lem  48214  lcoop  48599  lincvalsc0  48609  linc0scn0  48611  lincdifsn  48612  linc1  48613  lspsslco  48625  lincresunit3lem2  48668  lincresunit3  48669