Theorem pweqi 4567

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

Syntax hints:   = wceq 1541  𝒫 cpw 4551

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-ss 3916  df-pw 4553

This theorem is referenced by:  rankxplim  9782  pwdju1  10092  fin23lem17  10239  mnfnre  11165  qtopres  23623  hmphdis  23721  ust0  24145  made0  27828  umgrpredgv  29129  issubgr  29260  uhgrissubgr  29264  cusgredg  29413  cffldtocusgr  29436  cffldtocusgrOLD  29437  konigsbergiedgw  30239  shsspwh  31237  circtopn  33861  r11  35116  r12  35117  lfuhgr  35173  rankeq1o  36226  onsucsuccmpi  36498  bj-unirel  37106  elrfi  42801  islmodfg  43176  clsk1indlem4  44151  clsk1indlem1  44152  clsk1independent  44153  omef  46608  caragensplit  46612  caragenelss  46613  carageneld  46614  omeunile  46617  caragensspw  46621  0ome  46641  isomennd  46643  ovn02  46680  isuspgrimlem  48009  grtri  48054  usgrexmpl1lem  48135  usgrexmpl2lem  48140  lcoop  48526  lincvalsc0  48536  linc0scn0  48538  lincdifsn  48539  linc1  48540  lspsslco  48552  lincresunit3lem2  48595  lincresunit3  48596