Theorem pweqi 4638

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

Syntax hints:   = wceq 1537  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  pwfiOLD  9417  rankxplim  9948  pwdju1  10260  fin23lem17  10407  mnfnre  11333  qtopres  23727  hmphdis  23825  ust0  24249  made0  27930  umgrpredgv  29175  issubgr  29306  uhgrissubgr  29310  cusgredg  29459  cffldtocusgr  29482  cffldtocusgrOLD  29483  konigsbergiedgw  30280  shsspwh  31278  circtopn  33783  lfuhgr  35085  rankeq1o  36135  onsucsuccmpi  36409  bj-unirel  37017  elrfi  42650  islmodfg  43026  clsk1indlem4  44006  clsk1indlem1  44007  clsk1independent  44008  omef  46417  caragensplit  46421  caragenelss  46422  carageneld  46423  omeunile  46426  caragensspw  46430  0ome  46450  isomennd  46452  ovn02  46489  uspgrimprop  47757  isuspgrimlem  47758  grtri  47791  usgrexmpl1lem  47836  usgrexmpl2lem  47841  lcoop  48140  lincvalsc0  48150  linc0scn0  48152  lincdifsn  48153  linc1  48154  lspsslco  48166  lincresunit3lem2  48209  lincresunit3  48210