Theorem pweqi 4563

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

Syntax hints:   = wceq 1541  𝒫 cpw 4547

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-pw 4549

This theorem is referenced by:  rankxplim  9772  pwdju1  10082  fin23lem17  10229  mnfnre  11155  qtopres  23613  hmphdis  23711  ust0  24135  made0  27818  umgrpredgv  29118  issubgr  29249  uhgrissubgr  29253  cusgredg  29402  cffldtocusgr  29425  cffldtocusgrOLD  29426  konigsbergiedgw  30228  shsspwh  31226  circtopn  33850  r11  35105  r12  35106  lfuhgr  35162  rankeq1o  36215  onsucsuccmpi  36487  bj-unirel  37095  elrfi  42797  islmodfg  43172  clsk1indlem4  44147  clsk1indlem1  44148  clsk1independent  44149  omef  46604  caragensplit  46608  caragenelss  46609  carageneld  46610  omeunile  46613  caragensspw  46617  0ome  46637  isomennd  46639  ovn02  46676  isuspgrimlem  48005  grtri  48050  usgrexmpl1lem  48131  usgrexmpl2lem  48136  lcoop  48522  lincvalsc0  48532  linc0scn0  48534  lincdifsn  48535  linc1  48536  lspsslco  48548  lincresunit3lem2  48591  lincresunit3  48592