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 1540  𝒫 cpw 4551

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-pw 4553

This theorem is referenced by:  rankxplim  9775  pwdju1  10085  fin23lem17  10232  mnfnre  11158  qtopres  23583  hmphdis  23681  ust0  24105  made0  27787  umgrpredgv  29085  issubgr  29216  uhgrissubgr  29220  cusgredg  29369  cffldtocusgr  29392  cffldtocusgrOLD  29393  konigsbergiedgw  30192  shsspwh  31190  circtopn  33804  lfuhgr  35091  rankeq1o  36145  onsucsuccmpi  36417  bj-unirel  37025  elrfi  42667  islmodfg  43042  clsk1indlem4  44017  clsk1indlem1  44018  clsk1independent  44019  omef  46477  caragensplit  46481  caragenelss  46482  carageneld  46483  omeunile  46486  caragensspw  46490  0ome  46510  isomennd  46512  ovn02  46549  isuspgrimlem  47879  grtri  47924  usgrexmpl1lem  48005  usgrexmpl2lem  48010  lcoop  48396  lincvalsc0  48406  linc0scn0  48408  lincdifsn  48409  linc1  48410  lspsslco  48422  lincresunit3lem2  48465  lincresunit3  48466