Theorem pweqi 4557

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

Syntax hints:   = wceq 1542  𝒫 cpw 4541

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  rankxplim  9803  pwdju1  10113  fin23lem17  10260  mnfnre  11188  qtopres  23663  hmphdis  23761  ust0  24185  made0  27855  umgrpredgv  29209  issubgr  29340  uhgrissubgr  29344  cusgredg  29493  cffldtocusgr  29516  konigsbergiedgw  30318  shsspwh  31317  circtopn  33981  r11  35237  r12  35238  lfuhgr  35300  rankeq1o  36353  onsucsuccmpi  36625  bj-unirel  37358  elrfi  43126  islmodfg  43497  clsk1indlem4  44471  clsk1indlem1  44472  clsk1independent  44473  omef  46924  caragensplit  46928  caragenelss  46929  carageneld  46930  omeunile  46933  caragensspw  46937  0ome  46957  isomennd  46959  ovn02  46996  isuspgrimlem  48371  grtri  48416  usgrexmpl1lem  48497  usgrexmpl2lem  48502  lcoop  48887  lincvalsc0  48897  linc0scn0  48899  lincdifsn  48900  linc1  48901  lspsslco  48913  lincresunit3lem2  48956  lincresunit3  48957