Theorem pweqi 4572

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

Syntax hints:   = wceq 1542  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  rankxplim  9803  pwdju1  10113  fin23lem17  10260  mnfnre  11187  qtopres  23654  hmphdis  23752  ust0  24176  made0  27871  umgrpredgv  29225  issubgr  29356  uhgrissubgr  29360  cusgredg  29509  cffldtocusgr  29532  cffldtocusgrOLD  29533  konigsbergiedgw  30335  shsspwh  31334  circtopn  34015  r11  35271  r12  35272  lfuhgr  35334  rankeq1o  36387  onsucsuccmpi  36659  bj-unirel  37299  elrfi  43051  islmodfg  43426  clsk1indlem4  44400  clsk1indlem1  44401  clsk1independent  44402  omef  46854  caragensplit  46858  caragenelss  46859  carageneld  46860  omeunile  46863  caragensspw  46867  0ome  46887  isomennd  46889  ovn02  46926  isuspgrimlem  48255  grtri  48300  usgrexmpl1lem  48381  usgrexmpl2lem  48386  lcoop  48771  lincvalsc0  48781  linc0scn0  48783  lincdifsn  48784  linc1  48785  lspsslco  48797  lincresunit3lem2  48840  lincresunit3  48841