Theorem pweqi 4578

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

Syntax hints:   = wceq 1570  𝒫 cpw 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-pw 4564

This theorem is referenced by:  rankxplim  9847  pwdju1  10170  fin23lem17  10317  mnfnre  11247  qtopres  23855  hmphdis  23953  ust0  24377  made0  28056  umgrpredgv  29490  issubgr  29621  uhgrissubgr  29625  cusgredg  29774  cffldtocusgr  29797  konigsbergiedgw  30599  shsspwh  31598  circtopn  34227  r11  35487  r12  35488  lfuhgr  35610  rankeq1o  36663  onsucsuccmpi  36954  bj-unirel  37687  elrfi  43425  islmodfg  43796  clsk1indlem4  44770  clsk1indlem1  44771  clsk1independent  44772  omef  47210  caragensplit  47214  caragenelss  47215  carageneld  47216  omeunile  47219  caragensspw  47223  0ome  47243  isomennd  47245  ovn02  47282  isuspgrimlem  48660  grtri  48705  usgrexmpl1lem  48786  usgrexmpl2lem  48791  lcoop  49191  lincvalsc0  49201  linc0scn0  49203  lincdifsn  49204  linc1  49205  lspsslco  49217  lincresunit3lem2  49260  lincresunit3  49261