Theorem pweqi 4619

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

Syntax hints:   = wceq 1542  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  pwfiOLD  9347  rankxplim  9874  pwdju1  10185  fin23lem17  10333  mnfnre  11257  qtopres  23202  hmphdis  23300  ust0  23724  made0  27369  umgrpredgv  28431  issubgr  28559  uhgrissubgr  28563  cusgredg  28712  cffldtocusgr  28735  konigsbergiedgw  29532  shsspwh  30530  circtopn  32848  lfuhgr  34139  rankeq1o  35174  gg-cffldtocusgr  35230  onsucsuccmpi  35376  bj-unirel  35980  elrfi  41480  islmodfg  41859  clsk1indlem4  42843  clsk1indlem1  42844  clsk1independent  42845  omef  45260  caragensplit  45264  caragenelss  45265  carageneld  45266  omeunile  45269  caragensspw  45273  0ome  45293  isomennd  45295  ovn02  45332  lcoop  47140  lincvalsc0  47150  linc0scn0  47152  lincdifsn  47153  linc1  47154  lspsslco  47166  lincresunit3lem2  47209  lincresunit3  47210