Theorem pweqi 4570

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

Syntax hints:   = wceq 1541  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556

This theorem is referenced by:  rankxplim  9791  pwdju1  10101  fin23lem17  10248  mnfnre  11175  qtopres  23642  hmphdis  23740  ust0  24164  made0  27859  umgrpredgv  29213  issubgr  29344  uhgrissubgr  29348  cusgredg  29497  cffldtocusgr  29520  cffldtocusgrOLD  29521  konigsbergiedgw  30323  shsspwh  31321  circtopn  33994  r11  35250  r12  35251  lfuhgr  35312  rankeq1o  36365  onsucsuccmpi  36637  bj-unirel  37252  elrfi  42936  islmodfg  43311  clsk1indlem4  44285  clsk1indlem1  44286  clsk1independent  44287  omef  46740  caragensplit  46744  caragenelss  46745  carageneld  46746  omeunile  46749  caragensspw  46753  0ome  46773  isomennd  46775  ovn02  46812  isuspgrimlem  48141  grtri  48186  usgrexmpl1lem  48267  usgrexmpl2lem  48272  lcoop  48657  lincvalsc0  48667  linc0scn0  48669  lincdifsn  48670  linc1  48671  lspsslco  48683  lincresunit3lem2  48726  lincresunit3  48727