Theorem pweqi 4596

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

Syntax hints:   = wceq 1540  𝒫 cpw 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-pw 4582

This theorem is referenced by:  rankxplim  9898  pwdju1  10210  fin23lem17  10357  mnfnre  11283  qtopres  23641  hmphdis  23739  ust0  24163  made0  27842  umgrpredgv  29124  issubgr  29255  uhgrissubgr  29259  cusgredg  29408  cffldtocusgr  29431  cffldtocusgrOLD  29432  konigsbergiedgw  30234  shsspwh  31232  circtopn  33873  lfuhgr  35145  rankeq1o  36194  onsucsuccmpi  36466  bj-unirel  37074  elrfi  42684  islmodfg  43060  clsk1indlem4  44035  clsk1indlem1  44036  clsk1independent  44037  omef  46492  caragensplit  46496  caragenelss  46497  carageneld  46498  omeunile  46501  caragensspw  46505  0ome  46525  isomennd  46527  ovn02  46564  isuspgrimlem  47875  grtri  47919  usgrexmpl1lem  47992  usgrexmpl2lem  47997  lcoop  48354  lincvalsc0  48364  linc0scn0  48366  lincdifsn  48367  linc1  48368  lspsslco  48380  lincresunit3lem2  48423  lincresunit3  48424