Theorem pweqi 4515

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

Syntax hints:   = wceq 1538  𝒫 cpw 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  pwfi  8803  rankxplim  9292  pwdju1  9601  fin23lem17  9749  mnfnre  10673  qtopres  22303  hmphdis  22401  ust0  22825  umgrpredgv  26933  issubgr  27061  uhgrissubgr  27065  cusgredg  27214  cffldtocusgr  27237  konigsbergiedgw  28033  shsspwh  29029  circtopn  31190  lfuhgr  32477  rankeq1o  33745  onsucsuccmpi  33904  bj-unirel  34468  elrfi  39635  islmodfg  40013  clsk1indlem4  40747  clsk1indlem1  40748  clsk1independent  40749  omef  43135  caragensplit  43139  caragenelss  43140  carageneld  43141  omeunile  43144  caragensspw  43148  0ome  43168  isomennd  43170  ovn02  43207  lcoop  44820  lincvalsc0  44830  linc0scn0  44832  lincdifsn  44833  linc1  44834  lspsslco  44846  lincresunit3lem2  44889  lincresunit3  44890