Theorem pweqi 4621

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

Syntax hints:   = wceq 1537  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-pw 4607

This theorem is referenced by:  rankxplim  9917  pwdju1  10229  fin23lem17  10376  mnfnre  11302  qtopres  23722  hmphdis  23820  ust0  24244  made0  27927  umgrpredgv  29172  issubgr  29303  uhgrissubgr  29307  cusgredg  29456  cffldtocusgr  29479  cffldtocusgrOLD  29480  konigsbergiedgw  30277  shsspwh  31275  circtopn  33798  lfuhgr  35102  rankeq1o  36153  onsucsuccmpi  36426  bj-unirel  37034  elrfi  42682  islmodfg  43058  clsk1indlem4  44034  clsk1indlem1  44035  clsk1independent  44036  omef  46452  caragensplit  46456  caragenelss  46457  carageneld  46458  omeunile  46461  caragensspw  46465  0ome  46485  isomennd  46487  ovn02  46524  uspgrimprop  47811  isuspgrimlem  47812  grtri  47845  usgrexmpl1lem  47916  usgrexmpl2lem  47921  lcoop  48257  lincvalsc0  48267  linc0scn0  48269  lincdifsn  48270  linc1  48271  lspsslco  48283  lincresunit3lem2  48326  lincresunit3  48327