Theorem pweqi 4575

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

Syntax hints:   = wceq 1540  𝒫 cpw 4559

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 3446  df-ss 3928  df-pw 4561

This theorem is referenced by:  rankxplim  9808  pwdju1  10120  fin23lem17  10267  mnfnre  11193  qtopres  23618  hmphdis  23716  ust0  24140  made0  27822  umgrpredgv  29120  issubgr  29251  uhgrissubgr  29255  cusgredg  29404  cffldtocusgr  29427  cffldtocusgrOLD  29428  konigsbergiedgw  30227  shsspwh  31225  circtopn  33820  lfuhgr  35098  rankeq1o  36152  onsucsuccmpi  36424  bj-unirel  37032  elrfi  42675  islmodfg  43051  clsk1indlem4  44026  clsk1indlem1  44027  clsk1independent  44028  omef  46487  caragensplit  46491  caragenelss  46492  carageneld  46493  omeunile  46496  caragensspw  46500  0ome  46520  isomennd  46522  ovn02  46559  isuspgrimlem  47888  grtri  47932  usgrexmpl1lem  48005  usgrexmpl2lem  48010  lcoop  48393  lincvalsc0  48403  linc0scn0  48405  lincdifsn  48406  linc1  48407  lspsslco  48419  lincresunit3lem2  48462  lincresunit3  48463