Theorem pweqi 4581

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

Syntax hints:   = wceq 1541  𝒫 cpw 4565

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  pwfiOLD  9298  rankxplim  9824  pwdju1  10135  fin23lem17  10283  mnfnre  11207  qtopres  23086  hmphdis  23184  ust0  23608  made0  27246  umgrpredgv  28154  issubgr  28282  uhgrissubgr  28286  cusgredg  28435  cffldtocusgr  28458  konigsbergiedgw  29255  shsspwh  30251  circtopn  32507  lfuhgr  33798  rankeq1o  34832  onsucsuccmpi  34991  bj-unirel  35595  elrfi  41075  islmodfg  41454  clsk1indlem4  42438  clsk1indlem1  42439  clsk1independent  42440  omef  44857  caragensplit  44861  caragenelss  44862  carageneld  44863  omeunile  44866  caragensspw  44870  0ome  44890  isomennd  44892  ovn02  44929  lcoop  46612  lincvalsc0  46622  linc0scn0  46624  lincdifsn  46625  linc1  46626  lspsslco  46638  lincresunit3lem2  46681  lincresunit3  46682