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  23561  hmphdis  23659  ust0  24083  made0  27761  umgrpredgv  29043  issubgr  29174  uhgrissubgr  29178  cusgredg  29327  cffldtocusgr  29350  cffldtocusgrOLD  29351  konigsbergiedgw  30150  shsspwh  31148  circtopn  33800  lfuhgr  35078  rankeq1o  36132  onsucsuccmpi  36404  bj-unirel  37012  elrfi  42655  islmodfg  43031  clsk1indlem4  44006  clsk1indlem1  44007  clsk1independent  44008  omef  46467  caragensplit  46471  caragenelss  46472  carageneld  46473  omeunile  46476  caragensspw  46480  0ome  46500  isomennd  46502  ovn02  46539  isuspgrimlem  47868  grtri  47912  usgrexmpl1lem  47985  usgrexmpl2lem  47990  lcoop  48373  lincvalsc0  48383  linc0scn0  48385  lincdifsn  48386  linc1  48387  lspsslco  48399  lincresunit3lem2  48442  lincresunit3  48443