Theorem pweqi 4615

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

Syntax hints:   = wceq 1539  𝒫 cpw 4599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-pw 4601

This theorem is referenced by:  rankxplim  9920  pwdju1  10232  fin23lem17  10379  mnfnre  11305  qtopres  23707  hmphdis  23805  ust0  24229  made0  27913  umgrpredgv  29158  issubgr  29289  uhgrissubgr  29293  cusgredg  29442  cffldtocusgr  29465  cffldtocusgrOLD  29466  konigsbergiedgw  30268  shsspwh  31266  circtopn  33837  lfuhgr  35124  rankeq1o  36173  onsucsuccmpi  36445  bj-unirel  37053  elrfi  42710  islmodfg  43086  clsk1indlem4  44062  clsk1indlem1  44063  clsk1independent  44064  omef  46516  caragensplit  46520  caragenelss  46521  carageneld  46522  omeunile  46525  caragensspw  46529  0ome  46549  isomennd  46551  ovn02  46588  uspgrimprop  47878  isuspgrimlem  47879  grtri  47912  usgrexmpl1lem  47985  usgrexmpl2lem  47990  lcoop  48333  lincvalsc0  48343  linc0scn0  48345  lincdifsn  48346  linc1  48347  lspsslco  48359  lincresunit3lem2  48402  lincresunit3  48403